google flag issues - Githubissues

dreal / dreal2

Please check dreal4 instead.

https://github.com/dreal/dreal4

GNU General Public License v3.0

13 stars 15 forks source link

Open soonhokong opened 10 years ago

soonhokong commented 10 years ago

Google Flags Integrated. Known issues:

Gflags does not allow to have "-" in the middle of options. For instance, we can't have "--ode-grid" anymore. It has to be changed to "--ode_grid".
The messages with "--help" option is not so much user-friendly.