aboutsummaryrefslogtreecommitdiff
path: root/Makefile.install
diff options
context:
space:
mode:
authorRalf Treinen2020-03-10 21:36:04 +0100
committerRalf Treinen2020-03-10 21:36:09 +0100
commitd22db7a4a3c95bbbe6a4d7a25ed08f9d99fa64e8 (patch)
tree3c1fcade0a77b4b36c477982bf98119d519fed61 /Makefile.install
parent47862b094536cd9120fbad06c4733c95716c314d (diff)
test coq-makefile/findlib-package-unpacked: only try to invoke 'make' when
there is an ocamlopt compiler.
Diffstat (limited to 'Makefile.install')
0 files changed, 0 insertions, 0 deletions