From 36bcd20eb27287161c061ee1872ccb877a5387a7 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Mon, 27 Apr 1998 16:25:33 +0000
Subject: removed explicit reference to a binary in ctm's home directory

---
 lego.el | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/lego.el b/lego.el
index 75f1f9ba..fcd8776d 100644
--- a/lego.el
+++ b/lego.el
@@ -5,6 +5,9 @@
 
 
 ;; $Log$
+;; Revision 1.38  1998/04/27 16:25:33  tms
+;; removed explicit reference to a binary in ctm's home directory
+;;
 ;; Revision 1.37  1998/03/25 17:30:41  tms
 ;; added support for etags at generic proof level
 ;;
@@ -161,7 +164,7 @@
 
 ;; ----- lego-shell configuration options
 
-(defvar lego-prog-name "/home/ctm/lego/bin/legoML"
+(defvar lego-prog-name "lego"
   "*Name of program to run as lego.")
 
 (defvar lego-shell-working-dir ""
@@ -189,12 +192,11 @@
 (defvar lego-forget-id-command "Forget ")
 
 (defvar lego-undoable-commands-regexp
-  (ids-to-regexp '("\\`Dnf\\'" "Refine" "Intros" "intros" "Next" "Qrepl" "Claim"
-		   "For" "Repeat" "Succeed" "Fail" "Try" "Assumption" "UTac"
-		   "Qnify" "AndE" "AndI" "exE" "exI" "orIL" "orIR" "orE"
-		   "ImpI" "impE" "notI" "notE" "allI" "allE" "Expand"
-		   "Induction" "Immed"))
-  "Undoable list")
+  (ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal"
+  "Qrepl" "Claim" "For" "Repeat" "Succeed" "Fail" "Try" "Assumption"
+  "UTac" "Qnify" "AndE" "AndI" "exE" "exI" "orIL" "orIR" "orE" "ImpI"
+  "impE" "notI" "notE" "allI" "allE" "Expand" "Induction" "Immed"
+  "Invert")) "Undoable list")
 
 ;; ----- outline
 
-- 
cgit v1.2.3