diff options
| author | Ralf Treinen | 2020-03-10 21:36:04 +0100 |
|---|---|---|
| committer | Ralf Treinen | 2020-03-10 21:36:09 +0100 |
| commit | d22db7a4a3c95bbbe6a4d7a25ed08f9d99fa64e8 (patch) | |
| tree | 3c1fcade0a77b4b36c477982bf98119d519fed61 /dev/header.c | |
| parent | 47862b094536cd9120fbad06c4733c95716c314d (diff) | |
test coq-makefile/findlib-package-unpacked: only try to invoke 'make' when
there is an ocamlopt compiler.
Diffstat (limited to 'dev/header.c')
0 files changed, 0 insertions, 0 deletions