aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-17 22:12:27 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-17 22:12:27 +0000
commit52dad32c6bc3d5f9cbceb2bd0306d23dc279541b (patch)
treeaa888d3292d4086176ecb43446bf08ff34368d38 /generic
parent191202adabf2a9b6ea9f8ff389517940ae89f024 (diff)
Fix bug in replace-in-string for GNU Emacs
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-menu.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 93c7f49b..10da72a4 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -527,7 +527,7 @@ KEY is added onto proof-assistant map."
(define-key (proof-ass keymap) (quote ,key) (quote ,fn)))
(defun ,fn ()
,(concat "Shortcut command to insert "
- (replace-in-string string "\\\\" "\\=") ;; for substitute-command-keys
+ (replace-in-string string "\\\\" "\\\\=") ;; for substitute-command-keys
" into the current buffer.\nThis simply calls `proof-insert', which see.")
(interactive)
(proof-insert ,string))))
@@ -543,7 +543,7 @@ KEY is added onto proof-assistant map."
(define-key (proof-ass keymap) (quote ,key) (quote ,fn)))
(defun ,fn ()
,(concat "Command to send "
- (replace-in-string string "\\\\" "\\=") ;; for substitute-command-keys
+ (replace-in-string string "\\\\" "\\\\=") ;; for substitute-command-keys
" to the proof assistant.")
(interactive)
(proof-shell-invisible-command ,string))))