aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/checker.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index b2433ee36..cc285d5e4 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -329,6 +329,9 @@ let parse_args argv =
| ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
| ("-I"|"-include") :: [] -> usage ()
+ | "-Q" :: d :: p :: rem -> set_rec_include d p;parse rem
+ | "-Q" :: ([] | [_]) -> usage ()
+
| "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
| "-R" :: ([] | [_]) -> usage ()