diff options
| author | Gaëtan Gilbert | 2019-02-13 13:22:24 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-18 14:43:36 +0100 |
| commit | 0a465063a5501d9a84088fff8b1c8a62f63feec3 (patch) | |
| tree | c3408be3830a2815a302de0fcb004db3c1941bfb /doc/tools | |
| parent | f8d6c322783577b31cf55f8b55568ac56104202b (diff) | |
Add diff rule for README.rst to dune refman-html alias
We change regen_readme such that when given an argument it outputs
there instead of overwriting the readme.
Prompted by me noticing I forgot to regen in #9553.
Diffstat (limited to 'doc/tools')
| -rwxr-xr-x | doc/tools/coqrst/regen_readme.py | 15 |
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 "" |
