diff options
| author | Emilio Jesus Gallego Arias | 2019-05-25 20:52:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-25 20:52:30 +0200 |
| commit | 51dc650f8b47a7381c19376793871817f2ef9578 (patch) | |
| tree | 95baa9812c7aade24e4197b52d1c0aa3252d229f | |
| parent | 9241a6e25ff132a27762963b06ae1095c783c25f (diff) | |
| parent | f6811213b24b5646404d3f3ad48a4ec79eb12dab (diff) | |
Merge PR #10244: Coqc: Treat unknown arguments starting with dash as unknown options rather than files
Reviewed-by: ejgallego
| -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 = |