diff options
| author | Gan Shen | 2019-03-25 17:39:28 +0800 |
|---|---|---|
| committer | GitHub | 2019-03-25 17:39:28 +0800 |
| commit | 6785dd0f8cdf026830c8893532f0cf4674ce376d (patch) | |
| tree | 9123b2234271e93bc3c516691cc40f705595e41c | |
| parent | f9932e152d4e545ce095350d399a1d93862bc543 (diff) | |
Fix indentation
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 1505662306..695dea222f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1430,7 +1430,7 @@ with the same physical-to-logical translation and with an empty logical prefix. The command line option ``-R`` is a variant of ``-Q`` which has the strictly same behavior regarding loadpaths, but which also makes the corresponding ``.vo`` files available through their short names in a way - not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R path Lib`` +not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R path Lib`` associates to the file ``/path/fOO/Bar/File.vo`` the logical name ``Lib.fOO.Bar.File``, but allows this file to be accessed through the short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with |