aboutsummaryrefslogtreecommitdiff
path: root/todo
diff options
context:
space:
mode:
authorDavid Aspinall1999-09-29 15:44:53 +0000
committerDavid Aspinall1999-09-29 15:44:53 +0000
commit29f6b9e091e896d98505a0aa62dcac13f8896343 (patch)
tree9e9ad69837a8f30a47db57c69b1e0391b970e6a3 /todo
parent73b915389935f843839ad33f120c47cd60ee0d22 (diff)
Added proof-script-command-separator. Needs work.
Diffstat (limited to 'todo')
-rw-r--r--todo3
1 files changed, 3 insertions, 0 deletions
diff --git a/todo b/todo
index b4625739..f0e2e8e8 100644
--- a/todo
+++ b/todo
@@ -57,6 +57,9 @@ A Usability enhancement:
- Fix asymmetry between "doing" and "undoing": doing will skip comments,
undoing will not. e.g. test case: (* tester *) intros;
+A Usability enhancement:
+ - Fix proof-script-command-separator and proof-one-command-per-line flag.
+
C Compatibility enhancement:
- Consider sending comments to proof process after all. They might
contain special (e.g. LaTeX) directives or something.