aboutsummaryrefslogtreecommitdiffhomepage
path: root/todo
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-05-12 17:28:52 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-05-12 17:28:52 +0000
commitce7ed629d5d43cce6b3118cdbc6244c70b8e4113 (patch)
tree4260559a469590558be97b21d6aed2d05d7ec2bd /todo
parentada49d04eccf9f94831ad7498cac436ecfbffd40 (diff)
Notes about fixing docstring-magic.
Diffstat (limited to 'todo')
-rw-r--r--todo7
1 files changed, 7 insertions, 0 deletions
diff --git a/todo b/todo
index 80bfdf75..3ccb19c2 100644
--- a/todo
+++ b/todo
@@ -27,6 +27,13 @@ D e.g. desirable to fix at some point
X (Low) e.g. probably not worth spending time on
+*** Extremely urgent bits
+
+A Fix docstring-magic somehow so that multiple instances of PG can
+ be loaded at the same time. Looks like will have to redefine
+ the proof-assistant specific settings one by one, before calling
+ the specific code.
+
*** Outstanding bugs to investigate
A find C-c C-l binding and remove it. Overriden with goto-end-of-locked.