summaryrefslogtreecommitdiff
path: root/opam
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@google.com>2019-02-17 19:33:14 -0500
committerGravatar Benjamin Barenblat <bbaren@google.com>2019-02-17 19:33:14 -0500
commit01c0849f6bfb9ee6d2a57bb53da69eade2fa37e9 (patch)
treeb22e9cc6ecf86127b286bd81a9789263f9578567 /opam
parent3bc01565f84b4ddadc3962dc16dce22b4f36457a (diff)
Fix build on platforms without ocamlopt
coq_makefile generates Makefiles that reference ocamlopt, even on platforms without ocamlopt. Export `OPT=-byte` on such platforms to prevent the generated Makefile from trying to invoke ocamlopt.
Diffstat (limited to 'opam')
0 files changed, 0 insertions, 0 deletions