aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol98
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-03-10 09:20:35 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-03-10 09:20:35 +0000
commit2cce0bc0f772d120b9ad53b9241c78767ac727d0 (patch)
treead52380346a68bb3bd6c5e1267f4684231793553 /hol98
parent7ec2a7d39e2bdd3bfc9186fb44e7c7782bd39171 (diff)
TODOs for HOL.
Diffstat (limited to 'hol98')
-rw-r--r--hol98/todo12
1 files changed, 12 insertions, 0 deletions
diff --git a/hol98/todo b/hol98/todo
new file mode 100644
index 00000000..44179369
--- /dev/null
+++ b/hol98/todo
@@ -0,0 +1,12 @@
+-*- mode:outline -*-
+
+* See also ../todo for generic things to do, priority codes.
+
+* Things to do for HOL
+======================
+
+A Problem with displaying long help message: causes loop in PG
+ filtering, why? Process also takes a long time to kill off.
+
+B Improve display to strip ugly val it's.
+