From cfab9406e175a4d22c9441d1d7ba757cfd754887 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 12 Sep 2000 16:59:56 +0000
Subject: Remove shell important setting from script ones.

---
 generic/proof-script.el | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 8cbc167a..a3b7d63e 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2809,9 +2809,8 @@ a generic implementation of this."
 ;; Sanity checks on important settings
 ;;
 
-(defvar proof-script-important-settings
-  '(proof-shell-annotated-prompt-regexp ; crucial
-    proof-terminal-char			; soon not to be essential
+(defconst proof-script-important-settings
+  '(proof-terminal-char			; soon not to be essential
     proof-comment-start			;
     proof-comment-end
     ; proof-goal-command-regexp	  not needed if proof-goal-command-p is set
-- 
cgit v1.2.3