aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqc.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-01-24 14:37:45 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-01-26 14:20:52 +0100
commit8c0f9b63cb923a6cb6682124cd48db5da391075c (patch)
treec34f2972e3e336528648e5d0457de68b5e719e29 /tools/coqc.ml
parent3afdca3562b9dcadd9b16991bd8716f38a55f2c8 (diff)
-schedule-vi-checking ported to spawn
Diffstat (limited to 'tools/coqc.ml')
-rw-r--r--tools/coqc.ml8
1 files changed, 7 insertions, 1 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 5e63322c5..dbfdc40a2 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -71,6 +71,7 @@ let usage () =
exit 1
(* parsing of the command line *)
+let extra_arg_needed = ref true
let parse_args () =
let rec parse (cfiles,args) = function
@@ -150,6 +151,11 @@ let parse_args () =
| "-R" :: s :: "-as" :: t :: rem -> parse (cfiles,t::"-as"::s::"-R"::args) rem
| "-R" :: s :: "-as" :: [] -> usage ()
| "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
+ | ("-schedule-vi-checking" |"-check-vi-tasks" as o) :: s :: rem ->
+ let nodash, rem =
+ CList.split_when (fun x -> String.length x > 1 && x.[0] = '-') rem in
+ extra_arg_needed := false;
+ parse (cfiles, List.rev nodash @ s :: o :: args) rem
(* Anything else is interpreted as a file *)
@@ -172,7 +178,7 @@ let parse_args () =
let main () =
let cfiles, args = parse_args () in
- if cfiles = [] then begin
+ if cfiles = [] && !extra_arg_needed then begin
prerr_endline "coqc: too few arguments" ;
usage ()
end;