aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES8
-rw-r--r--generic/proof-menu.el1
2 files changed, 7 insertions, 2 deletions
diff --git a/CHANGES b/CHANGES
index 567b79a2..a1dce5bc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,8 +6,6 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
* Changes of Proof General 4.4.1 from Proof General 4.4
-* Changes of Proof General 4.4.1 from Proof General 4.4
-
** Generic changes
*** bug fixes
@@ -21,6 +19,12 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
useful as we can expect users to configure electric-terminator
once and for all. Hence the removal of this default key-binding.
+*** add another (fallback) key-binding for proof-goto-point
+ - The default key-binding for proof-goto-point (C-c <C-return>)
+ was not available in TTYs. Now, this function can also be run
+ with "C-c RET", which happens to be automatically trigerred if
+ we type "C-c <C-return>" in a TTY.
+
** Coq changes
*** new menu Coq -> Auto Compilation for all background compilation options
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 0a7317cb..35c6eb3b 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -113,6 +113,7 @@ without adjusting window layout."
;; C-c C-v is proof-minibuffer-cmd in universal-keys
;; C-c C-. is proof-goto-end-of-locked in universal-keys
(define-key map [(control c) (control return)] 'proof-goto-point)
+ (define-key map [(control c) (control m)] 'proof-goto-point) ; fallback for tty
(define-key map [(control c) ?v] 'pg-toggle-visibility)
(define-key map [(control meta mouse-3)] 'proof-mouse-goto-point)
;; NB: next binding overwrites comint-find-source-code.