diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2006-09-05 15:13:17 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2006-09-05 15:13:17 +0000 |
| commit | 07088a47b162ebc8b46acb53d0fc3b4e0e9d1dc6 (patch) | |
| tree | 1db01d8621a7f02259a86358c71da5de87c1e066 /generic/proof-config.el | |
| parent | 3817b477032a4fc82dd9df9b6e26c82ca77106e8 (diff) | |
Error highliting in coq now works
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 5 |
1 files changed, 4 insertions, 1 deletions
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) |