diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-30 18:05:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-08-02 15:06:53 +0200 |
| commit | 1eb48ca8695a26fa5ca248a2201a164f90885360 (patch) | |
| tree | 10e488654dff10055efeb63cbd941b35b7fa7646 /toplevel/usage.ml | |
| parent | 71e0a34f89d03787003df1a30bb793bd71ebb775 (diff) | |
For convenience, making yes and on, and no and off synonymous in
command line. Documenting only the former for simplicity and
uniformity with predating option -with-geoproof.
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f3f8dfd8a..a5d8450b9 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -58,7 +58,7 @@ let print_usage_channel co command = \n\ \n -quiet unset display of extra information (implies -w none)\ \n -w (all|none) configure display of warnings\ -\n -color (on|off|auto) configure color output\ +\n -color (yes|no|auto) configure color output\ \n\ \n -q skip loading of rcfile\ \n -init-file f set the rcfile to f\ |