Skip to content

Commit

Permalink
XXX fix more tests.
Browse files Browse the repository at this point in the history
  • Loading branch information
Rodolphe Lepigre committed Nov 4, 2024
1 parent c025041 commit 8ef6f3d
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -45,5 +45,5 @@ This test is currently broken due to the workspace resolution being faulty #5899
1 | (coq.theory
2 | (name foo))
Error: 'coq.theory' is available only when coq is enabled in the dune-project
file. You must enable it using (using coq 0.9) in your dune-project file.
file. You must enable it using (using coq 0.10) in your dune-project file.
[1]
2 changes: 1 addition & 1 deletion test/blackbox-tests/test-cases/coq/github3624.t
Original file line number Diff line number Diff line change
Expand Up @@ -17,5 +17,5 @@ good when the coq extension is not enabled.
1 | (coq.theory
2 | (name foo))
Error: 'coq.theory' is available only when coq is enabled in the dune-project
file. You must enable it using (using coq 0.9) in your dune-project file.
file. You must enable it using (using coq 0.10) in your dune-project file.
[1]

0 comments on commit 8ef6f3d

Please sign in to comment.