Skip to content

Commit 23ce99c

Browse files
committed
coq-tests: fix error introduced by Cyril Anaclet in 0ae25c5
The purpose of unwind-protect is to execute the cleanup-forms in case of a non-local exit. It does not make any sense to move these forms behind unwind-protect.
1 parent 1f07248 commit 23ce99c

File tree

1 file changed

+7
-7
lines changed

1 file changed

+7
-7
lines changed

ci/coq-tests.el

+7-7
Original file line numberDiff line numberDiff line change
@@ -152,13 +152,13 @@ then evaluate the BODY function and finally tear-down (exit Coq)."
152152
(setq proof-splash-enable nil)
153153
(normal-mode) ;; or (coq-mode)
154154
(coq-set-flags t flags)
155-
(coq-mock body))))
156-
(coq-test-exit)
157-
(coq-set-flags nil flags)
158-
(not-modified nil) ; Clear modification
159-
(kill-buffer buffer)
160-
(when rmfile (message "Removing file %s ..." rmfile))
161-
(ignore-errors (delete-file rmfile)))))
155+
(coq-mock body)))
156+
(coq-test-exit)
157+
(coq-set-flags nil flags)
158+
(not-modified nil) ; Clear modification
159+
(kill-buffer buffer)
160+
(when rmfile (message "Removing file %s ..." rmfile))
161+
(ignore-errors (delete-file rmfile))))))
162162

163163
(defun coq-test-goto-before (comment)
164164
"Go just before COMMENT (a unique string in the .v file).

0 commit comments

Comments
 (0)