diff options
| author | Robert Rand | 2019-05-07 12:44:09 -0400 |
|---|---|---|
| committer | GitHub | 2019-05-07 12:44:09 -0400 |
| commit | f958d281ab57acfb37e69bbe92ed603d87962ce6 (patch) | |
| tree | 7f3723115dbbc2b14861d1d88c9766c5ed1a3815 /doc | |
| parent | e30d52a3c724a71bf43b46416c09e4b6ef1d1f67 (diff) | |
Added description of Q
Note that this description is identical to that of R. R should maybe start with the word "Recursively"?
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 35231610fe..f799091af3 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -911,11 +911,13 @@ Command line options Coq``. :-R dir coqdir: 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. |