aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol-light
diff options
context:
space:
mode:
authorGravatar Clément Pit-Claudel <cpitclaudel@gmail.com>2017-05-05 10:22:25 -0400
committerGravatar GitHub <noreply@github.com>2017-05-05 10:22:25 -0400
commit409a116b00a2208e0fbc528981176d29c7966db6 (patch)
tree64131a91074063c119f10aa63d044d3011813c47 /hol-light
parent8038b7270e7fd9752a62be2b4e59f26b8d0e48dc (diff)
parentf607be020b5d5ebbca5a5b8a2cea2e234cace966 (diff)
Merge pull request #157 from ProofGeneral/elpa
[WIP] ELPA/MELPA support
Diffstat (limited to 'hol-light')
-rw-r--r--hol-light/hol-light-autotest.el8
1 files changed, 3 insertions, 5 deletions
diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el
index 20c16727..5c1cb011 100644
--- a/hol-light/hol-light-autotest.el
+++ b/hol-light/hol-light-autotest.el
@@ -8,14 +8,12 @@
(eval-when-compile
(require 'cl))
-(eval-when (compile)
- (require 'proof-site)
- (proof-ready-for-assistant 'coq)
- (defvar coq-compile-before-require nil))
+(require 'proof-site)
+(proof-ready-for-assistant 'hol-light)
(require 'pg-autotest)
-(unless noninteractive
+(unless (bound-and-true-p byte-compile-current-file)
(pg-autotest start 'debug)
(pg-autotest log ".autotest.log") ; convention