Re: What is -gtoggle useful for?

[Dominique Dhumieres]

Diego,

> In fact, it'd be nice to hide some other flags, but that's another problem.

Absolutely, I think the user flags should be well separated from the 
developer ones.

Cheers

Dominique