diff options
author | 2003-06-05 09:11:55 +0000 | |
---|---|---|
committer | 2003-06-05 09:11:55 +0000 | |
commit | 4a08cc1298e4598eb9060c6eb617c6a6ac76835c (patch) | |
tree | cf2381b004d69b487cac6e19e7f7d18fb32d2b41 /CHANGES | |
parent | b65d2de563c6927371c7bc4f663f2e565b924451 (diff) |
Updated.
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 7 |
1 files changed, 7 insertions, 0 deletions
@@ -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 |