From a2ef60931a194ee441ed0edd5bac68eed3179c50 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 29 Apr 2020 11:29:26 +0200
Subject: fix: ERT tests OK in batch & interactive mode at once

---
 ci/coq-tests.el | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index fe3510e0..5c1e7d83 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -71,7 +71,7 @@
   "Ensure `coq' is loaded."
   (unless (featurep 'coq)
     (add-to-list 'load-path
-		 (locate-dominating-file buffer-file-name "proof-general.el"))
+		 (locate-dominating-file coq-test-dir "proof-general.el"))
     (load "proof-general")
     (proofgeneral "coq")))
 
@@ -151,7 +151,10 @@ then evaluate the BODY function and finally tear-down (exit Coq)."
             (progn
               (coq-test-init)
               (with-current-buffer buffer
+                (setq proof-splash-enable nil)
+                (normal-mode) ;; or (coq-mode)
                 (coq-mock body)))
+          (coq-test-exit)
           (kill-buffer buffer)
           (when rmfile (message "Removing file %s ..." rmfile))
           (ignore-errors (delete-file rmfile))))))
-- 
cgit v1.2.3