aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol98
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-03-19 06:42:24 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-03-19 06:42:24 +0000
commit776750c813a39954259f5eb098259b5c124afd8c (patch)
treec98e812ab0caa542de5d9901d3accad1fe8dcdd6 /hol98
parent5ef0dfc6bc323f84aa8d47359d89c9057545f202 (diff)
Updated
Diffstat (limited to 'hol98')
-rw-r--r--hol98/todo9
1 files changed, 7 insertions, 2 deletions
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.