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 /debian | |
| 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 'debian')
| -rwxr-xr-x | debian/rules | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/debian/rules b/debian/rules index c235160..d39b8c6 100755 --- a/debian/rules +++ b/debian/rules @@ -12,6 +12,8 @@ INSTALL_TARGET := install-byte ifeq ($(OCAML_NATDYNLINK),yes) TARGET += opt INSTALL_TARGET += install +else + export OPT := -byte endif %: |