Summary: FAQ about copying output into new buffers

1 files changed, 15 insertions, 2 deletions

diff --git a/FAQ b/FAQ
index c96e6d48..92370801 100644
--- a/FAQ
+++ b/FAQ
@@ -1,5 +1,5 @@
-FAQs for using Proof General 
-============================
+FAQs for using/installing Proof General 
+=======================================
 
 With thanks to the anonymous authors of questions/answers below.
 
@@ -8,6 +8,19 @@ Please also check the BUGS file.
 
 -----------------------------------------------------------------
 
+Q. The prover process produces some useful output I'd like to
+   keep a note of, how do I do that?
+
+A. Some people cut and paste into comments in their source files.
+   But you can easily make new files or temporary buffers in Emacs:
+
+    * copy text from *response* or *goals* buffer
+    * C-x b <enter new name> RET
+    * Switch to correct mode, e.g.: M-x isar-response-mode RET
+    * Paste text, the highlighting/sumbols should appear correctly.
+
+-----------------------------------------------------------------
+
 Q. Proof General fails to load with an error message on start-up,
     containing text like this: