Removed traces of support for Ruy's legogrep. This is superseded by legotags.

1 files changed, 0 insertions, 8 deletions

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)