aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2003-06-05 09:11:55 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2003-06-05 09:11:55 +0000
commit4a08cc1298e4598eb9060c6eb617c6a6ac76835c (patch)
treecf2381b004d69b487cac6e19e7f7d18fb32d2b41 /CHANGES
parentb65d2de563c6927371c7bc4f663f2e565b924451 (diff)
Updated.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES7
1 files changed, 7 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 2b4764a8..470a305d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -67,6 +67,13 @@ Instead the menu reflects the current minor mode status; toggling it
will also update the default "global for PG" behaviour for new script
buffers.
+*** Movement of cursor on interrupt is disabled
+
+By default, the cursor jumps to the end of the locked region on an
+error. Previously it also jumped on an interrupt. This is configurable
+via `proof-shell-handle-error-or-interrupt-hook', which see.
+
+
*** Proof General -> Options menu changes
**** Improvement to options handling