diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2011-12-27 13:15:58 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2011-12-27 13:15:58 +0000 |
| commit | e388da31dddc2f2b99935b9ef6a064c088a91894 (patch) | |
| tree | df3eded6933d10234de8236758ef7242cae6b8f4 | |
| parent | 5a754170ca3113295a1bd58f407a2e40e05cc3ff (diff) | |
Extra test
| -rw-r--r-- | coq/coq-autotest.el | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index 0c8bccf3..4d00045f 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -20,8 +20,9 @@ (pg-autotest start 'debug) ;; new multiple file handling for Coq gives interactive queries - ;; continually unless we set this + ;; continually unless we set this. (setq proof-auto-action-when-deactivating-scripting 'retract) + (setq proof-no-fully-processed-buffer t) (pg-autotest log ".autotest.log") ; convention @@ -31,9 +32,11 @@ (pg-autotest script-wholefile "coq/example.v") (pg-autotest script-wholefile "coq/example-tokens.v") (pg-autotest script-wholefile "coq/ex-module.v") + (proof-shell-wait) (pg-autotest remark "Regression testing bug cases...") (pg-autotest script-wholefile "etc/coq/parsingcheck-410.v") + (pg-autotest script-wholefile "etc/coq/parsingcheck-412.v") (pg-autotest remark "Testing prove-as-you-go (not replay)") (find-file ".autotest.v") |