diff options
| author | Gaëtan Gilbert | 2019-10-13 18:17:06 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-14 10:24:40 +0200 |
| commit | 3f5417422b7498514a148242979431aa2990c584 (patch) | |
| tree | b1664e0e831627a25ecee9317cfc15932f4dc96b /doc/plugin_tutorial/README.md | |
| parent | 81216e8947fb4906f5a2b109cbed3e2584383c57 (diff) | |
test-suite/Makefile: work when manually involved for dune-compiled Coq
i.e. you can do
~~~
make -f Makefile.dune world
make -C test-suite success
~~~
to make just the success tests, then modify Coq sources and retest
just the ones you want
Diffstat (limited to 'doc/plugin_tutorial/README.md')
0 files changed, 0 insertions, 0 deletions