diff options
| author | Clément Pit-Claudel | 2018-08-28 12:03:05 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2018-08-28 12:03:05 -0400 |
| commit | 7e614ee91a9e5f67bab7dce0ff64dcae9a2a2419 (patch) | |
| tree | 96fc21d35a3eb3712f6fd4add823e76c98bbc0d4 /doc | |
| parent | a57891211e578605f6cb7e05f5fdadd7de49e519 (diff) | |
| parent | 53eb027a6b9e1c3322db1750e613470e07407a81 (diff) | |
Merge PR #8281: Trivial Sphinx fix in doc.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 88da58c27d..4e42bddee2 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -90,8 +90,8 @@ not set, they look for the commands in the executable path. The ``$COQ_COLORS`` environment variable can be used to specify the set of colors used by ``coqtop`` to highlight its output. It uses the same syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated -list of assignments of the form ``name=``:n:``{*; attr}`` where -``name`` is the name of the corresponding highlight tag and each ``attrᵢ`` is an +list of assignments of the form :n:`name={*; attr}` where +``name`` is the name of the corresponding highlight tag and each ``attr`` is an ANSI escape code. The list of highlight tags can be retrieved with the ``-list-tags`` command-line option of ``coqtop``. |
