diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2000-04-07 15:42:22 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2000-04-07 15:42:22 +0000 |
commit | 9424534f43284d294c199cc8beffa3dea59ef7cb (patch) | |
tree | cefeb675fc0415eb6e72ce4238a5c09c259df3a8 /todo | |
parent | 4a1571975d281f536d6e7deaef4ae4016140e5b4 (diff) |
Updated
Diffstat (limited to 'todo')
-rw-r--r-- | todo | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -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. |