From 0a465063a5501d9a84088fff8b1c8a62f63feec3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 13 Feb 2019 13:22:24 +0100
Subject: 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.
---
 doc/tools/coqrst/regen_readme.py | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'doc/tools')

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 ""
 
-- 
cgit v1.2.3