aboutsummaryrefslogtreecommitdiffhomepage
path: root/todo
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-04-07 15:42:22 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-04-07 15:42:22 +0000
commit9424534f43284d294c199cc8beffa3dea59ef7cb (patch)
treecefeb675fc0415eb6e72ce4238a5c09c259df3a8 /todo
parent4a1571975d281f536d6e7deaef4ae4016140e5b4 (diff)
Updated
Diffstat (limited to 'todo')
-rw-r--r--todo1
1 files changed, 1 insertions, 0 deletions
diff --git a/todo b/todo
index d895c997..3a08f012 100644
--- a/todo
+++ b/todo
@@ -71,6 +71,7 @@ X (Low) e.g. probably not worth spending time on
**** C More flexible help configuration is needed. HOL has some nice
on-line help but no way in PG to help by library. Perhaps
a help browser is needed? At least, optional arg to help command.
+ [patch ready and waiting to go in]
**** D Remove pbp.el, unused file.