aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall1998-10-21 13:21:32 +0000
committerDavid Aspinall1998-10-21 13:21:32 +0000
commite8e21ab2643638c8409e9ef04e72bcd9c1715a07 (patch)
treefee33e119fee676147a6802517c2dbb2d5f79d6b
parent0a65616e2685437f57b41ca8f6a83782f3d5f71d (diff)
Added todo for save-some-buffers
-rw-r--r--todo5
1 files changed, 4 insertions, 1 deletions
diff --git a/todo b/todo
index 78ac4df1..89c395c1 100644
--- a/todo
+++ b/todo
@@ -21,7 +21,10 @@ A* Fixup multiple files -- needs debugging.
(partly fixed)
2. Improve test for locked region being whole of buffer
(probably fixed)
- 3. Management of proof-script-buffer-list maybe wrong.
+ 3. Add save-some-buffers or similar to try to make sure that a
+ modified buffer is saved before it can be read to the prover.
+ If a buffer is put onto the proof-included-files-list when it is
+ modified, we should warn the user about possible inconsistency.
(3hrs)