aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2021-04-23 14:56:24 +0200
committerHugo Herbelin2021-04-23 15:00:57 +0200
commit7e0c8172703111a026477cf704f50af9468f8f0a (patch)
tree0b0a7a6b00049ded0b91295e6de96682a1b20049
parentc3d7754ec2045a964974698821adb73c586b4e41 (diff)
test-suite: add approve-coqdoc to update all coqdoc output files at once.
-rw-r--r--test-suite/Makefile11
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 2a2f62e23f..f06439a863 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -517,6 +517,17 @@ approve-output: output output-coqtop output-coqchk
echo "Updated $${f%.real}!"; \
done
+approve-coqdoc: coqdoc
+ $(HIDE)(cd coqdoc; \
+ for f in *.html.out; do \
+ cp "Coqdoc.$${f%.out}" "$$f"; \
+ echo "Updated $$f!"; \
+ done; \
+ for f in *.tex.out; do \
+ cat "Coqdoc.$${f%.out}" | grep -v "^%%" > "$$f"; \
+ echo "Updated $$f!"; \
+ done)
+
# the expected output for the MExtraction test is
# /plugins/micromega/micromega.ml except with additional newline
output/MExtraction.out: ../plugins/micromega/micromega.ml