diff options
| author | Théo Zimmermann | 2019-05-08 18:19:26 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-08 18:19:26 +0200 |
| commit | 86fd245bfd5c9750b515ea4204b0a9a50c14d930 (patch) | |
| tree | 87360584dbe021de790e427db009e7c676ec771b | |
| parent | 1d135d8005d6af37e0965db3f555b03db92546fd (diff) | |
| parent | 8f7559931d79588328049586b389d4109c59a9d2 (diff) | |
Merge PR #10087: Added description of Q
Reviewed-by: Zimmi48
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 35231610fe..554f6bf230 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -909,13 +909,15 @@ Command line options :--coqlib url: Set base URL for the Coq standard library (default is `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url Coq``. - :-R dir coqdir: Map physical directory dir to |Coq| logical + :-R dir coqdir: Recursively map physical directory dir to |Coq| logical directory ``coqdir`` (similarly to |Coq| option ``-R``). + :-Q dir coqdir: Map physical directory dir to |Coq| logical + directory ``coqdir`` (similarly to |Coq| option ``-Q``). .. note:: - option ``-R`` only has - effect on the files *following* it on the command line, so you will + options ``-R`` and ``-Q`` only have + effect on the files *following* them on the command line, so you will probably need to put this option first. |