From ce7ed629d5d43cce6b3118cdbc6244c70b8e4113 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 12 May 2000 17:28:52 +0000
Subject: Notes about fixing docstring-magic.

---
 todo | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'todo')

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.
-- 
cgit v1.2.3