From 9c0f36adac233efb1164ef88c86c78c7509d8b2c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 29 Nov 2017 14:57:33 +0100
Subject: Documenting the -Q flag of coqchk.

---
 checker/checker.ml        | 4 +++-
 doc/refman/RefMan-com.tex | 7 +++++--
 man/coqchk.1              | 8 ++++++--
 3 files changed, 14 insertions(+), 5 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\
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index b4d9f60eb..04a8a25c1 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -331,9 +331,12 @@ code, it cannot be guaranteed that the produced compiled libraries are
 correct. {\tt coqchk} is a standalone verifier, and thus it cannot be
 tainted by such malicious code.
 
-Command-line options {\tt -I}, {\tt -R}, {\tt -where} and
+Command-line options {\tt -Q}, {\tt -R}, {\tt -where} and
 {\tt -impredicative-set} are supported by {\tt coqchk} and have the
-same meaning as for {\tt coqtop}. Extra options are:
+same meaning as for {\tt coqtop}. As there is no notion of relative paths in
+object files {\tt -Q} and {\tt -R} have exactly the same meaning.
+
+Extra options are:
 \begin{description}
 \item[{\tt -norec} {\em module}]\ %
 
diff --git a/man/coqchk.1 b/man/coqchk.1
index a00914eab..f9241c0d4 100644
--- a/man/coqchk.1
+++ b/man/coqchk.1
@@ -34,12 +34,16 @@ add directory
 in the include path
 
 .TP
-.BI \-R \ dir\ coqdir          
-recursively map physical
+.BI \-Q \ dir\ coqdir
+map physical
 .I dir
 to logical
 .I coqdir
 
+.TP
+.BI \-R \ dir\ coqdir
+synonymous for -Q
+
 .TP
 .BI \-silent
 makes coqchk less verbose.
-- 
cgit v1.2.3