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/sphinx/dune | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'doc/sphinx/dune')

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