From 776750c813a39954259f5eb098259b5c124afd8c Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 19 Mar 2000 06:42:24 +0000 Subject: Updated --- hol98/todo | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'hol98') diff --git a/hol98/todo b/hol98/todo index 359c1195..6f8f6f95 100644 --- a/hol98/todo +++ b/hol98/todo @@ -4,8 +4,13 @@ See also ../todo for generic things to do, priority codes. -** A Problem with displaying long help message: causes loop in PG - filtering, why? Process also takes a long time to kill off. +** A Problem with process filtering. + + Process (sometimes?) doesn't recover after interrupt, and no output + is seen. Why? + + Also problem with some input texts: try interactive version of + clScript.sml, inductive defn of CL terms breaks things. ** B Improve display to strip ugly val it and spurious >'s. -- cgit v1.2.3