aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar Erik Martin-Dorel <erik@martin-dorel.org>2016-09-25 00:25:34 +0200
committerGravatar Erik Martin-Dorel <erik@martin-dorel.org>2016-09-25 00:25:34 +0200
commit71be0c69ff955b2e79f456b6dad5c4406fc08e71 (patch)
treeb63fc619d1d9bc3843a17e8da4f2a415dbccf5d5 /generic
parentdf812155800f2fb3aea39a936a6420dc79a3a501 (diff)
proof-retract-before-change: Fix #41 by saving/restoring the match data.
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-script.el11
1 files changed, 6 insertions, 5 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index a9c55353..e67a7774 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1989,11 +1989,12 @@ No effect if prover is busy."
(proof-interrupt-process)
(proof-shell-wait))
(save-excursion
- (save-restriction ;; see Trac#403
- (widen)
- (goto-char beg)
- (proof-retract-until-point)
- (proof-shell-wait)))))
+ (save-match-data ;; see PG#41
+ (save-restriction ;; see Trac#403
+ (widen)
+ (goto-char beg)
+ (proof-retract-until-point)
+ (proof-shell-wait))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;