diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2012-09-02 21:30:23 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2012-09-02 21:30:23 +0000 |
| commit | 6945689cefadbd46258d3cebad4eeb8790f485be (patch) | |
| tree | 211d10c2cbf33d96bb2a6767cf1d789757e9386b | |
| parent | 5f5a679974161c41db5ec9e93275ae861c25f56b (diff) | |
Remove ref to file parsingcheck-412.v missing from CVS, so "make coq.autotest" runs again
| -rw-r--r-- | coq/coq-autotest.el | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index 4d00045f..b6b361ed 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -8,12 +8,13 @@ (eval-when-compile (require 'cl)) +(require 'pg-autotest) + (eval-when (compile) (require 'proof-site) (proof-ready-for-assistant 'coq) (defvar coq-compile-before-require nil)) -(require 'pg-autotest) (unless noninteractive @@ -36,7 +37,7 @@ (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 script-wholefile "etc/coq/parsingcheck-412.v") (pg-autotest remark "Testing prove-as-you-go (not replay)") (find-file ".autotest.v") |