diff options
| author | Hugo Herbelin | 2019-05-11 16:17:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-14 11:27:15 +0200 |
| commit | df98a88a1e35213e994ec583f6ad4e0d3ccac868 (patch) | |
| tree | fb2fce0e40a14de61299bb98c420b6ed0b800292 | |
| parent | 9a49153b2104e8d7ca0d7789b47299295272746c (diff) | |
CoqIDE: Treat unknown arguments starting with dash as unknown options rather than files.
| -rw-r--r-- | ide/idetop.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml index ce00ba6d8c..970d7cf650 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -537,7 +537,11 @@ let rec parse = function Xmlprotocol.document Xml_printer.to_string_fmt; exit 0 | "--xml_format=Ppcmds" :: rest -> msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest - | x :: rest -> x :: parse rest + | x :: rest -> + if String.length x > 0 && x.[0] = '-' then + (prerr_endline ("Unknown option " ^ x); exit 1) + else + x :: parse rest | [] -> [] let () = Usage.add_to_usage "coqidetop" |