aboutsummaryrefslogtreecommitdiff
path: root/todo
diff options
context:
space:
mode:
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.