From 2c6843f8dd71d509a3ab7eb3ee68e8eb8dc5dac8 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 30 May 2011 15:13:32 +0000
Subject: Trac#403: wait for retraction to complete before returning, to avoid
 hitting read only error in calling command.

---
 generic/proof-script.el | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'generic/proof-script.el')

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)))))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-- 
cgit v1.2.3