From 07088a47b162ebc8b46acb53d0fc3b4e0e9d1dc6 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 5 Sep 2006 15:13:17 +0000
Subject: Error highliting in coq now works

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

(limited to 'generic')

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 45748ee1..6ea95171 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -2314,7 +2314,10 @@ values for this hook include:
  proof-goto-end-of-locked-if-pos-not-visible-in-window
 
 which move the cursor in the scripting buffer on an error or
-error/interrupt."
+error/interrupt.
+
+Remark: This hook is called from response buffer. If you want to do
+something in scripting buffer, save excursion and switch buffer."
   :type '(repeat function)
   :group 'proof-shell)
 
-- 
cgit v1.2.3