diff options
| author | James R. Wilcox | 2018-11-24 13:22:50 -0800 |
|---|---|---|
| committer | James R. Wilcox | 2018-11-24 13:22:50 -0800 |
| commit | 09b917593e90233d7a55610e9ce7886de77ef576 (patch) | |
| tree | cf1978d1778ef454d94bc8cf1c75f3954d3058e1 /doc/plugin_tutorial/tuto1/src/dune | |
| parent | b8c4bf77c19670099b1fea44f3ab6204faa25d6b (diff) | |
tests/Makefile: support unset COQBIN, like top-level Makefile does
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/dune')
0 files changed, 0 insertions, 0 deletions