From 258294f034ddf00d19a6225c090e78329da69f23 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Wed, 16 Dec 1998 14:35:47 +0000
Subject: documented LEGO specific bug

---
 BUGS | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'BUGS')

diff --git a/BUGS b/BUGS
index 28578b2e..5585ca68 100644
--- a/BUGS
+++ b/BUGS
@@ -67,6 +67,11 @@ FSF Emacs specific bugs
 LEGO Proof General Bugs
 =======================
 
+* If LEGO attempts to write a (object) file in a non-writable
+  directory, it forgets the protocol mechanism on how to interact with 
+  Proof General and gets stuck. Workaround: directly enter "Configure
+  AnnotateOn" in the Proof Shell to recover.
+
 * After a `Discharge', retraction ought to only be possible back to the
 first declaration/definition which is discharged. However, LEGO Proof
 General does not know that Discharge has such a non-local effect.
-- 
cgit v1.2.3