diff options
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 8 |
2 files changed, 7 insertions, 3 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index d3d75dddd8..efb5df720a 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -259,6 +259,8 @@ use antialiased fonts or not, by setting the environment variable `GDK_USE_XFT` to 1 or 0 respectively. +.. _coqide-unicode: + Bindings for input of Unicode symbols ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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. |