diff options
| author | Ralf Treinen | 2020-03-10 21:33:16 +0100 |
|---|---|---|
| committer | Ralf Treinen | 2020-03-10 21:33:35 +0100 |
| commit | 47862b094536cd9120fbad06c4733c95716c314d (patch) | |
| tree | 446d10ac35252cd421be6183d9c6cd9fb0119157 /dev/include_printers | |
| parent | 3a5469b2097c55ecf952ead470caf03b6112cd9e (diff) | |
test coq-makefile/camldep: try to build a cmx only when there is an ocamlopt
compiler. In any case, try to build a cmo file.
Diffstat (limited to 'dev/include_printers')
0 files changed, 0 insertions, 0 deletions