aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES6
-rw-r--r--generic/proof-script.el7
2 files changed, 10 insertions, 3 deletions
diff --git a/CHANGES b/CHANGES
index 4ac96315..142d3d84 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,6 +12,12 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
- Using query-replace (or replace-string) in the processed region
doesn't wrongly jump to the first match anymore.
+*** remove key-binding for proof-electric-terminator-toggle
+ - The default key-binding for proof-electric-terminator-toggle
+ (C-c .) was too easy to enter by mistake. And it was not that
+ useful as we can expect users to configure electric-terminator
+ once and for all. Hence the removal of this default key-binding.
+
** Coq changes
*** new menu Coq -> Auto Compilation for all background compilation options
diff --git a/generic/proof-script.el b/generic/proof-script.el
index e67a7774..7d9afe22 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2565,9 +2565,10 @@ finish setup which depends on specific proof assistant configuration."
;; Additional key def for (first character of) terminal string
(if proof-terminal-string
(progn
- (define-key proof-mode-map
- (vconcat [(control c)] (vector (aref proof-terminal-string 0)))
- 'proof-electric-terminator-toggle)
+;; This key-binding was disabled following a request in PG issue #160.
+;; (define-key proof-mode-map
+;; (vconcat [(control c)] (vector (aref proof-terminal-string 0)))
+;; 'proof-electric-terminator-toggle)
(define-key proof-mode-map (vector (aref proof-terminal-string 0))
'proof-electric-terminator)))