From b6ee807756b265d4b13b4a6452ad5d5095fe7e46 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 16 Nov 1999 21:55:35 +0000
Subject: Not strictly necessary to set proof-goal-command-regexp

---
 generic/proof-script.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'generic/proof-script.el')

diff --git a/generic/proof-script.el b/generic/proof-script.el
index fbdbaf71..c7d98503 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2591,7 +2591,7 @@ a generic implementation of this."
   '(proof-terminal-char
     proof-comment-start
     proof-comment-end
-    proof-goal-command-regexp
+    ; proof-goal-command-regexp	  not needed if proof-goal-command-p is set
     proof-save-command-regexp
     proof-goal-with-hole-regexp		; non-essential?
     proof-save-with-hole-regexp		; non-essential?
-- 
cgit v1.2.3