aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/practical-tools
diff options
context:
space:
mode:
authorThéo Zimmermann2018-08-23 17:23:03 +0200
committerThéo Zimmermann2018-08-23 17:23:03 +0200
commit05d13bf516a75da38bacbb62608528f8dceb34fd (patch)
tree9413e533937a1a10cebc9f6540289c1c69a58214 /doc/sphinx/practical-tools
parentc0f74e3f967f0cc20709100091ee1a01e145f1cf (diff)
parent69c8917e3bdc8678baf1358ead549acff2f52ca2 (diff)
Merge PR #8296: Fix #8251: remove "the the" occurrences
Diffstat (limited to 'doc/sphinx/practical-tools')
-rw-r--r--doc/sphinx/practical-tools/coq-commands.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 0f51b3eba3..88da58c27d 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -107,7 +107,7 @@ and ``coqtop``, unless stated otherwise:
to the OCaml loadpath. See also: :ref:`names-of-libraries` and the
command Declare ML Module Section :ref:`compiled-files`.
:-Q *directory* dirpath: Add physical path *directory* to the list of
- directories where |Coq| looks for a file and bind it to the the logical
+ directories where |Coq| looks for a file and bind it to the logical
directory *dirpath*. The subdirectory structure of *directory* is
recursively available from |Coq| using absolute names (extending the
dirpath prefix) (see Section :ref:`qualified-names`).Note that only those