On Tue, Sep 22, 2009 at 10:15 AM, Michael Hanselmann <[email protected]> wrote: > > 2009/9/22 Iustin Pop <[email protected]>: >> I think we should either name them all flag_$blah (not so nice for >> cmdline) > > The command line or the LU could automatically add the “flag_” part to > all flags passed to it.
True as well. But do we actually gain anything, by that? Anyway, both are fine for me! :) Thanks, Guido
