From fc9af819f6faa4214c376f74a14e4db45178c921 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 27 Oct 1998 15:18:28 +0000
Subject: Moved pbp-goal-command and pbp-hyp-command to proof-config.Moved LEGO
 specifix.

---
 generic/proof-script.el | 4 ----
 1 file changed, 4 deletions(-)

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

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 4447f368..b423aed9 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1428,10 +1428,6 @@ finish setup which depends on specific proof assistant configuration."
   ;; calculate some strings and regexps for searching
   (setq proof-terminal-string (char-to-string proof-terminal-char))
 
-  ;; FIXME: these are LEGO specific!
-  (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string))
-  (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string))
-
   ;; FIXME da: I'm not sure we ought to add spaces here, but if
   ;; we don't, there would be trouble overloading these settings
   ;; to also use as regexps for finding comments.
-- 
cgit v1.2.3