aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--tools/coqc.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 90585c763..1d416a1c4 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -126,6 +126,7 @@ 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
+ | "-Q" :: s :: t :: rem -> parse (cfiles,t::s::"-Q"::args) rem
| ("-schedule-vi-checking"
|"-check-vi-tasks" | "-schedule-vi2vo" as o) :: s :: rem ->
let nodash, rem =