diff options
| author | Hugo Herbelin | 2019-05-07 09:12:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-14 11:37:50 +0200 |
| commit | eed3831a2cc32042fdee95767da00d7e52840371 (patch) | |
| tree | 6a862b88882897b87b4106df62ab6dce9888435d /toplevel | |
| parent | d4bb58a66ebaa771216524c070a090e60d4fb7a9 (diff) | |
Coqc: Ensure that at most one file is given when -o is also given.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqcargs.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index 0ccd68613f..2279ce5505 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -56,6 +56,13 @@ let error_missing_arg s = prerr_endline "See -help for the syntax of supported options"; exit 1 +let check_compilation_output_name_consistency args = + match args.compilation_output_name, args.compile_list with + | Some _, _::_::_ -> + prerr_endline ("Error: option -o is not valid when more than one"); + prerr_endline ("file have to be compiled") + | _ -> () + let add_compile ?echo copts s = (* make the file name explicit; needed not to break up Coq loadpath stuff. *) let echo = Option.default copts.echo echo in @@ -185,5 +192,7 @@ let parse arglist : t = in try let opts, extra = parse default in - List.fold_left add_compile opts extra + let args = List.fold_left add_compile opts extra in + check_compilation_output_name_consistency args; + args with any -> fatal_error any |