Skip to content

Commit

Permalink
Merge PR coq#19982: Missing spaces in documentation of rocq doc.
Browse files Browse the repository at this point in the history
Reviewed-by: proux01
Co-authored-by: proux01 <proux01@users.noreply.github.com>
  • Loading branch information
coqbot-app[bot] and proux01 authored Jan 3, 2025
2 parents 03dd829 + 8dc1aef commit 6c18649
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions doc/sphinx/using/tools/coqdoc.rst
Original file line number Diff line number Diff line change
Expand Up @@ -221,7 +221,7 @@ identifier is linked to the place of its definition.
file``. Take care of erasing this global file, if any, when starting
the whole compilation process.

Then invoke `rocq doc` or ``rocqdoc --glob-from file`` to tell `rocq doc` to look
Then invoke `rocq doc` or ``rocq doc --glob-from file`` to tell `rocq doc` to look
for name resolutions in the file ``file`` (it will look in ``file.glob``
by default).

Expand Down Expand Up @@ -286,7 +286,7 @@ Usage
~~~~~

`rocq doc` is invoked on a shell command line as follows:
``rocqdoc <options and files>``.
``rocq doc <options and files>``.
Any command line argument which is not an option is considered to be a
file (even if it starts with a ``-``). Rocq files are identified by the
suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``.
Expand Down

0 comments on commit 6c18649

Please sign in to comment.