From eed3831a2cc32042fdee95767da00d7e52840371 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 7 May 2019 09:12:58 +0200
Subject: Coqc: Ensure that at most one file is given when -o is also given.

---
 toplevel/coqcargs.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3