aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall1999-05-11 13:40:53 +0000
committerDavid Aspinall1999-05-11 13:40:53 +0000
commitfe99b102e8809974f791c992a5d643084fcdd4ce (patch)
tree9ff21d65e5a7540c01fd2d5b4a379bbb67f73c34
parentec5c2837767afcf0557a3cbd29b1b39b33676cc8 (diff)
todo for reorganizing menus.
-rw-r--r--todo3
1 files changed, 3 insertions, 0 deletions
diff --git a/todo b/todo
index 1e2d01cc..af5b4f24 100644
--- a/todo
+++ b/todo
@@ -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,