Skip to content

Commit

Permalink
test: promote coq tests
Browse files Browse the repository at this point in the history
Signed-off-by: Rudi Grinberg <[email protected]>
  • Loading branch information
rgrinberg committed Feb 8, 2022
1 parent 9ea4f73 commit 2e5fc74
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions test/blackbox-tests/test-cases/coq/github3624.t/run.t
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,9 @@ that the error message is good when the coq extension is not enabled.
> (name foo))
> EOF
$ dune build
Warning: No dune-project file has been found. A default one is assumed but
the project might break when dune is upgraded. Please create a dune-project
file.
File "dune", line 1, characters 0-24:
1 | (coq.theory
2 | (name foo))
Expand Down

0 comments on commit 2e5fc74

Please sign in to comment.