diff options
| author | Hugo Herbelin | 2015-07-30 18:05:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-08-02 15:06:53 +0200 |
| commit | 1eb48ca8695a26fa5ca248a2201a164f90885360 (patch) | |
| tree | 10e488654dff10055efeb63cbd941b35b7fa7646 | |
| 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.
| -rw-r--r-- | toplevel/coqtop.ml | 12 | ||||
| -rw-r--r-- | toplevel/usage.ml | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 5540dc0ff1..d67559d77f 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -41,8 +41,8 @@ let toploop = ref None let color : [`ON | `AUTO | `OFF] ref = ref `AUTO let set_color = function -| "on" -> color := `ON -| "off" -> color := `OFF +| "yes" | "on" -> color := `ON +| "no" | "off" -> color := `OFF | "auto" -> color := `AUTO | _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1 @@ -326,8 +326,8 @@ let get_priority opt s = prerr_endline ("Error: low/high expected after "^opt); exit 1 let get_async_proofs_mode opt = function - | "off" -> Flags.APoff - | "on" -> Flags.APon + | "no" | "off" -> Flags.APoff + | "yes" | "on" -> Flags.APon | "lazy" -> Flags.APonLazy | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 @@ -341,8 +341,8 @@ let set_worker_id opt s = Flags.async_proofs_worker_id := s let get_bool opt = function - | "yes" -> true - | "no" -> false + | "yes" | "on" -> true + | "no" | "off" -> false | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 let get_int opt n = diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f3f8dfd8ae..a5d8450b9d 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\ |