diff options
Diffstat (limited to 'BUGS')
| -rw-r--r-- | BUGS | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -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. |