aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRobert Rand2019-05-07 13:05:19 -0400
committerGitHub2019-05-07 13:05:19 -0400
commit8f7559931d79588328049586b389d4109c59a9d2 (patch)
tree7649eee71c28f09b3d1c3c02b8122223bf3210e3
parentf958d281ab57acfb37e69bbe92ed603d87962ce6 (diff)
Added "Recursively" for the R option
-rw-r--r--doc/sphinx/practical-tools/utilities.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index f799091af3..554f6bf230 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -909,7 +909,7 @@ 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``).