Added note about new FSF bug discovered, sigh...

2 files changed, 21 insertions, 0 deletions

diff --git a/BUGS b/BUGS
index 33da5239..e991be99 100644
--- a/BUGS
+++ b/BUGS
@@ -80,6 +80,13 @@ simplifier, when tracing rewriting.
 
 * Problems with particular Emacs versions
 
+** FSF Emacs hangs when undoing first command in script.
+ 
+Noticed with Emacs 20.6.1.  Seems to affect all provers.
+Workaround:  use C-c C-RET or C-c C-r instead.
+Nasty workaround: (setq debug-on-quit t), hit "c" on each hang
+to continue.
+
 ** XEmacs 21.1.9 on Win32
 
 Some strange problems reading files with this version of Emacs. Gives
diff --git a/todo b/todo
index 3a08f012..50f8b32f 100644
--- a/todo
+++ b/todo
@@ -27,6 +27,20 @@ D		e.g. desirable to fix at some point
 X (Low)		e.g. probably not worth spending time on
 
 
+*** Outstanding bugs to investigate
+
+C Undoing comments with FSF Emacs weirdness.
+ Noticed with Emacs 20.6.1.  Seems to affect all provers.
+ Workaround:  use C-c C-RET or C-c C-r instead.
+ Nasty workaround: (setq debug-on-quit t), hit "c" on each hang
+ to continue.
+ Seems to get stuck looping in {coq,lego,whetever}-find-and-forget
+ but no problem when running with edebug edebug-defun on this function.
+ Maybe filter specific glitch to do with spans?
+
+C Problem with startup for Coq and HOL.  See BUGS.
+
+
 *** Scheduled improvements for 3.2
 
 **** A Doc new bits: font lock keywords, filename %e, %r.