aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-11-29 14:57:33 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-12-01 09:53:27 +0100
commit9c0f36adac233efb1164ef88c86c78c7509d8b2c (patch)
treee80f268b8b1c68e2ec4736d5e86211ab0ae37fcd /checker
parenta4dce1658f9a946cedb40ddcf0cdbc5391dd2005 (diff)
Documenting the -Q flag of coqchk.
Diffstat (limited to 'checker')
-rw-r--r--checker/checker.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index 596d42b66..fee31b667 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -174,7 +174,9 @@ let print_usage_channel co command =
output_string co command;
output_string co "coqchk options are:\n";
output_string co
-" -R dir coqdir map physical dir to logical coqdir\
+" -Q dir coqdir map physical dir to logical coqdir\
+\n -R dir coqdir synonymous for -Q\
+\n\
\n\
\n -admit module load module and dependencies without checking\
\n -norec module check module but admit dependencies without checking\