diff options
Diffstat (limited to 'coq/coq-autotest.el')
| -rw-r--r-- | coq/coq-autotest.el | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index 6d268b3d..0e12d48c 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -1,6 +1,6 @@ -;; coq-autotest.el: tests of Isar Proof General. +;; coq-autotest.el: tests of Coq Proof General (in progress). ;; -;; You can run these by issuing "make devel.test.isar" in PG home dir. +;; You can run these by issuing "make test.coq" in PG home dir. ;; ;; $Id$ ;; @@ -8,12 +8,13 @@ (require 'pg-autotest) ;; The included test files -(pg-autotest message "Testing standard examples") -(pg-autotest script-wholefile "coq/example.v") -(pg-autotest script-wholefile "coq/example-x-symbol.v") -(pg-autotest script-wholefile "coq/ex-module.v") +(eval-when (load) + (pg-autotest message "Testing standard examples") + (pg-autotest script-wholefile "coq/example.v") + (pg-autotest script-wholefile "coq/example-x-symbol.v") + (pg-autotest script-wholefile "coq/ex-module.v") -(pg-autotest-quit-prover) -(pg-autotest-finished) + (pg-autotest-quit-prover) + (pg-autotest-finished)) |