aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2011-05-30 15:13:32 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2011-05-30 15:13:32 +0000
commit2c6843f8dd71d509a3ab7eb3ee68e8eb8dc5dac8 (patch)
tree11d409229edfa25a5ab2ccac43d044aa356b4eb9 /generic
parent22295d5e6520cfd025feebb4b000fde2c41fadd4 (diff)
Trac#403: wait for retraction to complete before returning, to
avoid hitting read only error in calling command.
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-script.el3
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 9e4562c4..e6a2a65e 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1980,7 +1980,8 @@ No effect if prover is busy."
(save-restriction ;; see Trac#403
(widen)
(goto-char beg)
- (proof-retract-until-point)))))
+ (proof-retract-until-point)
+ (proof-shell-wait)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;