aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-autotest.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq-autotest.el')
-rw-r--r--coq/coq-autotest.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index a5b35ba4..a179a596 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -8,7 +8,7 @@
(require 'pg-autotest)
;; The included test files
-(unless (noninteractive)
+(unless noninteractive
(pg-autotest message "Testing standard examples")
(pg-autotest script-wholefile "coq/example.v")
(pg-autotest script-wholefile "coq/example-x-symbol.v")