documented LEGO specific bug

1 files changed, 5 insertions, 0 deletions

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.