diff options
| author | Gaëtan Gilbert | 2018-08-22 15:53:09 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-08-22 15:53:09 +0200 |
| commit | 69c8917e3bdc8678baf1358ead549acff2f52ca2 (patch) | |
| tree | a6887ed23653b143ce28482bc661fab1b495a60e /doc/sphinx/practical-tools | |
| parent | a62ab4903d61b9a3c2e8725ee0e6354c0a073348 (diff) | |
Fix #8251: remove "the the" occurrences
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 2 |
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 |