From 00b7706d4bb5f285e0efbca031e27b4bcf36aa50 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Fri, 2 Oct 1998 13:28:05 +0000
Subject: added LEGO support for proof-goal-command and proof-save-command

---
 generic/proof.el | 4 ++--
 lego/lego.el     | 2 ++
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/generic/proof.el b/generic/proof.el
index 45f10ce6..bec4bd71 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -1860,7 +1860,7 @@ insert when called interactively.")
   (interactive
    (if proof-goal-command 
        (if (stringp proof-goal-command)
-	   (list (format proof-goal-command-string
+	   (list (format proof-goal-command
 			 (read-string "Goal: " ""
 				      proof-issue-goal-history)))
 	 (proof-goal-command))
@@ -1877,7 +1877,7 @@ insert when called interactively.")
   (interactive
    (if proof-save-command
        (if (stringp proof-save-command)
-	   (list (format proof-save-command-string
+	   (list (format proof-save-command
 			 (read-string "Save as: " ""
 				      proof-issue-save-history)))
 	 (proof-save-command))
diff --git a/lego/lego.el b/lego/lego.el
index 372d779d..de053166 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -392,6 +392,8 @@
 	proof-www-home-page lego-www-home-page)
 
   (setq proof-prf-string "Prf"
+	proof-goal-command "Goal %s;"
+	proof-save-command "Save %s;"
 	proof-ctxt-string "Ctxt"
 	proof-help-string "Help")
 
-- 
cgit v1.2.3