diff options
| author | Théo Zimmermann | 2019-02-18 19:51:57 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-18 19:51:57 +0100 |
| commit | 7c62153610f54a96cdded0455af0fff7ff91a53a (patch) | |
| tree | 2633a2162326439e990f9ab7cf9d7259a6358ddf /doc/sphinx/dune | |
| parent | a4a59ec5cf426bb1ee36dc1ac49cb20bd17d5f43 (diff) | |
| parent | 0a465063a5501d9a84088fff8b1c8a62f63feec3 (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/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))) |