From 588314e72d2b390da057a30d6aa9b9cdc0f6ef07 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 26 Nov 1998 17:25:43 +0000
Subject: Warning in proof-shell-insert-hook docstrings.

---
 generic/proof-config.el | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 413b4fa4..67deb0e4 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -795,7 +795,15 @@ The default value is \"\\n\" to match up to the end of the line."
 Can be used to configure the proof assistant to the interface in
 various ways (for example, setting the line width of output).
 Any text inserted by these hooks will be sent to the proof process
-before every command issued by Proof General."
+before every command issued by Proof General.
+
+NB: You should be very careful about setting this hook. 
+Proof General relies on a careful synchronization with
+the process between inputs and outputs.  It expects to see
+a prompt for each input it sends from the queue.  If your
+extra input here causes more prompts than expected, things
+will break!  Probably any insertions made should not have 
+carriage returns."
   :type '(repeat function)
   :group 'proof-shell)
 
-- 
cgit v1.2.3