Updated.

3 files changed, 35 insertions, 31 deletions

diff --git a/BUGS b/BUGS
index 27c6decf..60c9e877 100644
--- a/BUGS
+++ b/BUGS
@@ -12,29 +12,6 @@ PG menus may be added to wrong bar during autoload.  See CHANGES for
 temporary workaround.
 
 
-** UTF-8 problems with Red Hat 8.0 / glibc 2.2  and (at least) Coq.  
-
-RedHat 8 has glibc 2.2 and UTF8 encoded output may be turned on in
-default locale.  Unfortunately Proof General relies on 8-bit
-characters which are UTF8 prefixes in the output of proof assistants
-(inc Coq, Isabelle).  These prefix characters are not flushed to
-stdout individually.  As a workaround we must find a way to disable
-interpretation of UTF8 in the C libraries that Coq and friends use.
-
-Doing this inside PG/Emacs seems tricky; locale settings are
-set/inherited in strange ways.  One solution is to run the Emacs
-process itself in a different locale, for example, starting XEmacs by
-typing:
-
-  $  LANG=en_GB xemacs &
-
-Another solution is to set LANG inside a file ~/.i18n, which will
-be read the shell.  This will affect all applications, though.
-[ suggestions for a better workaround inside Emacs would be welcome ]
-
-
-
-
 =================================================================
 
 
diff --git a/FAQ b/FAQ
index a58b08ae..0a35c69a 100644
--- a/FAQ
+++ b/FAQ
@@ -5,6 +5,33 @@ For latest version, see http://www.proofgeneral.org/FAQ
 
 Credits to the anonymous authors of questions/answers below.
 
+Please also check the BUGS file.
+
+-----------------------------------------------------------------
+
+Q. Emacs appears to hang when the prover process is started.
+
+A. This may be because of UTF-8 issues e.g in Red Hat 8.0/9/glibc 2.2
+
+RedHat 8 has glibc 2.2 and UTF8 encoded output may be turned on in
+default locale.  Unfortunately Proof General relies on 8-bit
+characters which are UTF8 prefixes in the output of proof assistants
+(inc Coq, Isabelle).  These prefix characters are not flushed to
+stdout individually.  As a workaround we must find a way to disable
+interpretation of UTF8 in the C libraries that Coq and friends use.
+
+Doing this inside PG/Emacs seems tricky; locale settings are
+set/inherited in strange ways.  One solution is to run the Emacs
+process itself in a different locale, for example, starting XEmacs by
+typing:
+
+  $  LANG=en_GB xemacs &
+
+Another solution is to set LANG inside a file ~/.i18n, which will
+be read the shell.  This will affect all applications, though.
+[ suggestions for a better workaround inside Emacs would be welcome ]
+
+
 -----------------------------------------------------------------
 
 Q. XEmacs 21.4 displays a progress bar during fontification which
@@ -139,11 +166,10 @@ A. These are part of the 8 bit character codes used by X Symbol to
 
    To fix, type 
 
-	M-x font-lock-fontify-buffer 
+	M-x x-symbol-decode-recorde
 
-   or M-x x-symbol-fontify. If that doesn't work, type M-x
-   font-lock-mode twice to turn font-lock off then on. 
-   Or reload the file.
+   If that doesn't work, type M-x font-lock-mode twice to turn font-lock 
+   off then on.   Or reload the file.
    
    Note that X-Symbol is more robust when used with XEmacs/Mule.
 
diff --git a/etc/cvs-tips.txt b/etc/cvs-tips.txt
index a8b8fc7f..5566620d 100644
--- a/etc/cvs-tips.txt
+++ b/etc/cvs-tips.txt
@@ -15,10 +15,11 @@ dcs.ed.
 your passphrase as needed.  The point is that you don't want to
 keep typing passwords on every CVS command).
 
-2. The CVS repository for PG is in ~proofgen/src at dcs.ed.ac.uk To
-use this, you need to set CVSROOT and CVS_RSH.  I use the script below
-(the last line isn't essential but makes the settings inside a running
-emacs too)
+2. The CVS repository for PG is in ~proofgen/src at dcs.ed.ac.uk 
+
+To use this, you need to set CVSROOT and CVS_RSH.  I use the script
+below (the last line isn't essential but makes the settings inside a
+running emacs too)
 
 3. Where you want to develop PG, do: