aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol-light/hol-light-autotest.el
diff options
context:
space:
mode:
Diffstat (limited to 'hol-light/hol-light-autotest.el')
-rw-r--r--hol-light/hol-light-autotest.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el
index 20c16727..b9924c41 100644
--- a/hol-light/hol-light-autotest.el
+++ b/hol-light/hol-light-autotest.el
@@ -8,14 +8,14 @@
(eval-when-compile
(require 'cl))
-(eval-when (compile)
+(eval-when-compile
(require 'proof-site)
(proof-ready-for-assistant 'coq)
(defvar coq-compile-before-require nil))
(require 'pg-autotest)
-(unless noninteractive
+(unless (bound-and-true-p byte-compile-current-file)
(pg-autotest start 'debug)
(pg-autotest log ".autotest.log") ; convention