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.el30
1 files changed, 21 insertions, 9 deletions
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index b6b361ed..cecfdcf1 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -1,22 +1,30 @@
-;; coq-autotest.el: tests of Coq Proof General (in progress).
+;;; coq-autotest.el --- tests of Coq Proof General (in progress).
+
+;; This file is part of Proof General.
+
+;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
+;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc.
+;; Portions © Copyright 2001-2017 Pierre Courtieu
+;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
+;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
+;; Portions © Copyright 2015-2017 Clément Pit-Claudel
+
+;;; Commentary:
;;
;; You can run these by issuing "make test.coq" in PG home dir.
;;
-;; $Id$
-;;
+
+;;; Code:
(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 'proof-site)
+(defvar coq-compile-before-require)
-(unless noninteractive
+(unless (bound-and-true-p byte-compile-current-file)
(pg-autotest start 'debug)
@@ -89,3 +97,7 @@
(pg-autotest timetaken 'total)
(pg-autotest exit))
+
+(provide 'coq-autotest)
+
+;;; coq-autotest.el ends here