diff options
| author |  Benjamin Barenblat <bbaren@google.com> | 2019-02-17 19:33:14 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@google.com> | 2019-02-17 19:33:14 -0500 |
| commit | 01c0849f6bfb9ee6d2a57bb53da69eade2fa37e9 (patch) | |
| tree | b22e9cc6ecf86127b286bd81a9789263f9578567 /AAC_print.ml | |
| parent | 3bc01565f84b4ddadc3962dc16dce22b4f36457a (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 'AAC_print.ml')
0 files changed, 0 insertions, 0 deletions