Skip to content

Commit

Permalink
coq-par-compile: adapt coqdep warning regexp to 8.19
Browse files Browse the repository at this point in the history
  • Loading branch information
hendriktews committed Jan 5, 2024
1 parent ba755fd commit 36b1d28
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 4 deletions.
4 changes: 3 additions & 1 deletion CHANGES
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,9 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG

* Changes of Proof General 4.6 from Proof General 4.5

N/A
** Coq changes

*** support Coq 8.19

* Changes of Proof General 4.5 from Proof General 4.4

Expand Down
2 changes: 0 additions & 2 deletions ci/compile-tests/010-coqdep-errors/runtest.el
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,6 @@
;;; Define the tests

(ert-deftest cct-coqdep-fail-on-require ()
:expected-result (if (coq--post-v818) :failed :passed)
"coqdep error on missing library in a require command is detected."
;; (setq cct--debug-tests t)
;; (setq coq--debug-auto-compilation t)
Expand Down Expand Up @@ -97,7 +96,6 @@


(ert-deftest cct-coqdep-fail-on-require-in-dependency ()
:expected-result (if (coq--post-v818) :failed :passed)
"coqdep error because of a missing library in a dependency is detected."
(let (coqdep-errror-in-response
missing-module-in-response
Expand Down
2 changes: 1 addition & 1 deletion coq/coq-compile-common.el
Original file line number Diff line number Diff line change
Expand Up @@ -523,7 +523,7 @@ or not."
:safe (lambda (v) (cl-every #'stringp v)))

(defcustom coq-coqdep-error-regexp
(concat "^\\*\\*\\* Warning: in file .*, library .* is required "
(concat "^\\(\\*\\*\\* \\)?Warning: in file .*, library[ \n].* is required "
"and has not been found")
"Regexp to match errors in the output of coqdep.
coqdep indicates errors not always via a non-zero exit status,
Expand Down

0 comments on commit 36b1d28

Please sign in to comment.