diff options
| author | David Aspinall | 2000-04-07 15:42:22 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-04-07 15:42:22 +0000 |
| commit | 9424534f43284d294c199cc8beffa3dea59ef7cb (patch) | |
| tree | cefeb675fc0415eb6e72ce4238a5c09c259df3a8 | |
| parent | 4a1571975d281f536d6e7deaef4ae4016140e5b4 (diff) | |
Updated
| -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. |
