From c02b0a35ba391a7217421aeec2e59fabd49ac249 Mon Sep 17 00:00:00 2001 From: Gan Shen Date: Sun, 24 Mar 2019 18:01:00 +0800 Subject: Fix typo --- doc/sphinx/language/gallina-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 18cafd1f21..99391950c3 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1431,7 +1431,7 @@ 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 `). For instance, ``-R`` `path` ``Lib`` -associates to the file path `path`\ ``/path/fOO/Bar/File.vo`` the logical name +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 identical base name are present in different subdirectories of a -- cgit v1.2.3 From f9932e152d4e545ce095350d399a1d93862bc543 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 25 Mar 2019 16:55:07 +0800 Subject: Update doc/sphinx/language/gallina-extensions.rst Co-Authored-By: gshen42 --- doc/sphinx/language/gallina-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 99391950c3..1505662306 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 `). For instance, ``-R`` `path` ``Lib`` + not unlike the ``Import`` command (see :ref:`here `). 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 -- cgit v1.2.3 From 6785dd0f8cdf026830c8893532f0cf4674ce376d Mon Sep 17 00:00:00 2001 From: Gan Shen Date: Mon, 25 Mar 2019 17:39:28 +0800 Subject: Fix indentation --- doc/sphinx/language/gallina-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 `). For instance, ``-R path Lib`` +not unlike the ``Import`` command (see :ref:`here `). 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 -- cgit v1.2.3