aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-autotest.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2011-01-18 18:06:50 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2011-01-18 18:06:50 +0000
commitaade2c8a764cfb9c82389e8275c2013bcdb0e6c7 (patch)
tree3e2bfcb40f01fe273a1652132fa400d3e28905ef /coq/coq-autotest.el
parent83eda1e681d8b20a017ceaa5b0d9625be82dcd0b (diff)
Add multiple file test case
Diffstat (limited to 'coq/coq-autotest.el')
-rw-r--r--coq/coq-autotest.el12
1 files changed, 12 insertions, 0 deletions
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index 9efdea22..fdfa5f1d 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -65,6 +65,18 @@
(pg-autotest quit-prover)
+ (pg-autotest remark "Testing multiple-file recompilation...")
+ (pg-autotest script-wholefile "coq/ex/test-cases/multiple-files-single-dir/f.v")
+ (proof-shell-wait)
+ ;; touch d.v to cause recompile (TODO: check for that)
+ (find-file "d.v")
+ (set-buffer-modified-p t)
+ (save-buffer)
+ (pg-autotest-test-retract-file "coq/ex/test-cases/multiple-files-single-dir/f.v")
+ (proof-shell-wait)
+ (pg-autotest script-wholefile "coq/ex/test-cases/multiple-files-single-dir/f.v")
+
+ (pg-autotest quit-prover)
(pg-autotest remark "Complete.")
(pg-autotest timetaken 'total)