diff options
| author | Emilio Jesus Gallego Arias | 2018-11-28 00:47:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-28 01:17:07 +0100 |
| commit | e2fe373a1947206746dd43afe6c9815c69453def (patch) | |
| tree | 94333b1e21124e4394dbd722276c37a62662f7a7 /doc/plugin_tutorial/tuto1/src/dune | |
| parent | 550472c67198353120cdc02b42683024b5b39765 (diff) | |
[build] Test tests in Travis, use coqc for tests.
`coqtop -batch` is an oxymoron, in prevision for upstream changes use
`coqc`.
We also call `make test` in Travis as to make CI more robust.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/dune')
0 files changed, 0 insertions, 0 deletions