Suggest to change LC_CTYPE rather than LANG. Thanks to Achim Brucker.

1 files changed, 34 insertions, 31 deletions

diff --git a/FAQ b/FAQ
index 7454c328..53806223 100644
--- a/FAQ
+++ b/FAQ
@@ -8,6 +8,40 @@ 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 and later 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 with an altered locale setting, for example,
+   starting XEmacs by typing:
+
+   $  LC_CTYPE=en_GB xemacs &
+
+   The supplied proofgeneral script makes this setting if it sees
+   the string UTF in the current value of LC_CTYPE.
+
+   Alternatively you can set LC_CTYPE 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 ]
+
+   NB: a related issue is warnings from x-symbol: "Emacs language 
+   environment and system locale specify different encoding, I'll 
+   assume `iso-8859-1'".  This warning appears to be mainly harmless.
+   Notice that the variable `buffer-file-coding-system' may determine
+   the format that files are saved in.  
+
+-----------------------------------------------------------------
+
 Q. Proof General fails to load with an error message on start-up: 
 
      error: "File `.../ProofGeneral/generic/proof-autoloads.elc' was 
@@ -58,37 +92,6 @@ beginning their names with a space.  So if you are looking for
 
 -----------------------------------------------------------------
 
-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 and later 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 ]
-
-   NB: a related issue is warnings from x-symbol: "Emacs language 
-   environment and system locale specify different encoding, I'll 
-   assume `iso-8859-1'".  This warning appears to be mainly harmless.
-   Notice that the variable `buffer-file-coding-system' may determine
-   the format that files are saved in.  
-
------------------------------------------------------------------
-
 Q. Help, I'm stuck!! Emacs keeps telling me "Cannot switch buffers in a
    dedicated window"