From caa100e2d95bc81af6edc74bc969e1d4e13b7ca3 Mon Sep 17 00:00:00 2001 From: hendriktews Date: Tue, 5 Mar 2024 01:03:37 +0100 Subject: [PATCH] coq-tests: fix error introduced by Cyril Anaclet in 0ae25c5a (#743) 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. --- ci/coq-tests.el | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/ci/coq-tests.el b/ci/coq-tests.el index d7e2c7cd7..7f4291b16 100644 --- a/ci/coq-tests.el +++ b/ci/coq-tests.el @@ -152,13 +152,13 @@ then evaluate the BODY function and finally tear-down (exit Coq)." (setq proof-splash-enable nil) (normal-mode) ;; or (coq-mode) (coq-set-flags t flags) - (coq-mock body)))) - (coq-test-exit) - (coq-set-flags nil flags) - (not-modified nil) ; Clear modification - (kill-buffer buffer) - (when rmfile (message "Removing file %s ..." rmfile)) - (ignore-errors (delete-file rmfile))))) + (coq-mock body))) + (coq-test-exit) + (coq-set-flags nil flags) + (not-modified nil) ; Clear modification + (kill-buffer buffer) + (when rmfile (message "Removing file %s ..." rmfile)) + (ignore-errors (delete-file rmfile)))))) (defun coq-test-goto-before (comment) "Go just before COMMENT (a unique string in the .v file).