diff options
| author | Hugo Herbelin | 2019-05-25 15:48:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-25 15:48:40 +0200 |
| commit | f6811213b24b5646404d3f3ad48a4ec79eb12dab (patch) | |
| tree | f4610628ed2af78fc80ae010be3e1904156fe4f9 | |
| parent | 5727443376480be4793757fd5507621ad4f09509 (diff) | |
Coqc: Treat unknown arguments starting with dash as unknown options rather than files.
| -rw-r--r-- | toplevel/coqcargs.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index 2279ce5505..63c37e2251 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -63,7 +63,10 @@ let check_compilation_output_name_consistency args = prerr_endline ("file have to be compiled") | _ -> () +let is_dash_argument s = String.length s > 0 && s.[0] = '-' + let add_compile ?echo copts s = + if is_dash_argument s then (prerr_endline ("Unknown option " ^ s); exit 1); (* make the file name explicit; needed not to break up Coq loadpath stuff. *) let echo = Option.default copts.echo echo in let s = |