From b2fda763e66f354ed6dcbe93ac18ebee32d69c21 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Tue, 10 Nov 1998 13:14:42 +0000
Subject: Removed traces of support for Ruy's legogrep. This is superseded by
 legotags.

---
 todo | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'todo')

diff --git a/todo b/todo
index 0a8c3076..da2559bf 100644
--- a/todo
+++ b/todo
@@ -389,14 +389,6 @@ X pbp code doesn't quite accord with the tech report; in particular it
 
 C fix Pbp implementation (10h)
 
-B `lego-get-path' assumes that LEGOPATH has been set in the
-  environment. This is not likely to be the case with the current lego 
-  shell script. Proof General needs to query the LEGO process as part
-  of `lego-process-config' e.g. by
-  sending (a yet to be implemented command) LEGOPATH. The output could 
-  be analysed with the help of a LEGO specific extension of
-  `proof-shell-process-urgent-message'. (1h tms)
-
 B Equiv, Next,... aren't handled properly, because LEGO does not
   refresh the proof state. Perhaps it would be easiest to get LEGO to
   output more information in proof script mode (2h)
-- 
cgit v1.2.3