From 19962a677f2b26707a224e2864dec48b7d2b5de0 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Wed, 16 Sep 1998 14:40:18 +0000
Subject: Documentation acknowleges use of three type of buffers:

  script buffers, goal buffer and process buffer
---
 todo | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

(limited to 'todo')

diff --git a/todo b/todo
index 32315ba4..2a9115ed 100644
--- a/todo
+++ b/todo
@@ -203,15 +203,6 @@ X pbp code doesn't quite accord with the tech report; in particular it
 
 A fix Pbp implementation (10h; tms)
 
-A Error messages need to be revised e.g., if an import fails, LEGO
-  outputs
-
-    Error in file: search: undefined or out of context: should
-   (* closing file ./blah.l; time= 0.010000  gc= 0.0  sys= 0.0 *)
-   Error: Unwinding to top-level
-
-  but script management only prints the last line. (5h tms)
-
 A release new version of the LEGO proof engine (4h tms)
 
 B Equiv, Next,... aren't handled properly, because LEGO does not
@@ -224,7 +215,8 @@ B LEGO should not issue warning messages triggered by the interactive
     Lego> Module nstderror Import stderror;
     Including module nstderror
     Warning: module name "nstderror" does not equal filename ""!
-    Warning: Interactive use of Module command.
+
+  (15min)
 
 X Mechanism to save object file
 
@@ -313,3 +305,5 @@ A fix INSTALL file, add COPYING note
 A fix branches after renames
 
 A write Makefile targets to build documentation formats, .elc
+
+A write release message
\ No newline at end of file
-- 
cgit v1.2.3