Skip to content

Commit

Permalink
coq-tests: fix error introduced by Cyril Anaclet in 0ae25c5
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
hendriktews committed Mar 3, 2024
1 parent 1f07248 commit 23ce99c
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 deletions ci/coq-tests.el
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down

0 comments on commit 23ce99c

Please sign in to comment.