aboutsummaryrefslogtreecommitdiff
path: root/doc/tools
diff options
context:
space:
mode:
authorThéo Zimmermann2019-02-18 19:51:57 +0100
committerThéo Zimmermann2019-02-18 19:51:57 +0100
commit7c62153610f54a96cdded0455af0fff7ff91a53a (patch)
tree2633a2162326439e990f9ab7cf9d7259a6358ddf /doc/tools
parenta4a59ec5cf426bb1ee36dc1ac49cb20bd17d5f43 (diff)
parent0a465063a5501d9a84088fff8b1c8a62f63feec3 (diff)
Merge PR #9568: Add test that we regenerated doc/sphinx/README.rst to linter
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
Diffstat (limited to 'doc/tools')
-rwxr-xr-xdoc/tools/coqrst/regen_readme.py15
1 files changed, 11 insertions, 4 deletions
diff --git a/doc/tools/coqrst/regen_readme.py b/doc/tools/coqrst/regen_readme.py
index e56882a521..0c15d7334c 100755
--- a/doc/tools/coqrst/regen_readme.py
+++ b/doc/tools/coqrst/regen_readme.py
@@ -10,6 +10,17 @@ SCRIPT_DIR = path.dirname(path.abspath(__file__))
if __name__ == "__main__" and __package__ is None:
sys.path.append(path.dirname(SCRIPT_DIR))
+SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/")
+README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst")
+
+if len(sys.argv) == 1:
+ README_PATH = path.join(SPHINX_DIR, "README.rst")
+elif len(sys.argv) == 2:
+ README_PATH = sys.argv[1]
+else:
+ print ("usage: {} [FILE]".format(sys.argv[0]))
+ sys.exit(1)
+
import sphinx
from coqrst import coqdomain
@@ -23,10 +34,6 @@ def format_docstring(template, obj, *strs):
strs = strs + (FIRST_LINE_BLANKS.sub(r"\1\n", docstring),)
return template.format(*strs)
-SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/")
-README_PATH = path.join(SPHINX_DIR, "README.rst")
-README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst")
-
def notation_symbol(d):
return " :black_nib:" if issubclass(d, coqdomain.NotationObject) else ""