aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2000-04-07 15:42:22 +0000
committerDavid Aspinall2000-04-07 15:42:22 +0000
commit9424534f43284d294c199cc8beffa3dea59ef7cb (patch)
treecefeb675fc0415eb6e72ce4238a5c09c259df3a8
parent4a1571975d281f536d6e7deaef4ae4016140e5b4 (diff)
Updated
-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.