diff options
| author | David Aspinall | 1999-05-11 13:40:53 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-05-11 13:40:53 +0000 |
| commit | fe99b102e8809974f791c992a5d643084fcdd4ce (patch) | |
| tree | 9ff21d65e5a7540c01fd2d5b4a379bbb67f73c34 | |
| parent | ec5c2837767afcf0557a3cbd29b1b39b33676cc8 (diff) | |
todo for reorganizing menus.
| -rw-r--r-- | todo | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -115,6 +115,9 @@ B Check matching code carefully, in view of bug reported (now fixed) word matching is based on whitespace constituents or non-word constituents. [6 hrs] +C Reorganize menus in a better way. Have generic scripting commands + for keyboard or menu/toolbar use. (2hrs) + C Implement proof-auto-retract idea. (4hrs) C Make and test generic versions of <..>-goal-command-p, |
