aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2007-05-10 21:18:45 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2007-05-10 21:18:45 +0000
commit8001e07411bc763122cb54ae52d84b4503a102dd (patch)
tree58a96284705f36651459ee4be8cbec999e5c2110 /generic
parente6a2fe06d46ac9c4400e9e8f6bf974680a67e3f2 (diff)
pg-remove-specials: avoid interactive replace-regexp, which gives minibuffer messages.
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-utils.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 1bdf12bc..6c5b86e0 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -477,7 +477,7 @@ Leave point at END."
(if (and start end)
(narrow-to-region start end))
(goto-char (or start (point-min)))
- (replace-regexp pg-special-char-regexp "")
+ (proof-replace-regexp-nocasefold pg-special-char-regexp "")
(goto-char (point-max))))
(defun pg-remove-specials-in-string (string)