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/sphinx/dune | |
| 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/sphinx/dune')
| -rw-r--r-- | doc/sphinx/dune | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/sphinx/dune b/doc/sphinx/dune index fff025c919..353d58c676 100644 --- a/doc/sphinx/dune +++ b/doc/sphinx/dune @@ -1 +1,8 @@ (dirs :standard _static) + +(rule (targets README.gen.rst) + (deps (source_tree ../tools/coqrst) README.template.rst) + (action (run ../tools/coqrst/regen_readme.py %{targets}))) + +(alias (name refman-html) + (action (diff README.rst README.gen.rst))) |