diff options
| author |  Benjamin Barenblat <bbaren@google.com> | 2019-02-17 20:22:08 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@google.com> | 2019-02-17 20:22:08 -0500 |
| commit | 0714858a81915fc118d7563e7ffc467c6221f086 (patch) | |
| tree | baf2e94a31e44fe9d9638182b9264cddec8e7a3a | |
| parent | 01c0849f6bfb9ee6d2a57bb53da69eade2fa37e9 (diff) | |
Fix install on platforms without ocamlopt
I was a bit overzealous in d10b86dc97e91ceb15134cc190d6f647a7c3d640,
changing `make install` to `make install-byte` on bytecode platforms.
Turns out both `make install` and `make install-byte` install important
files on both native and bytecode platforms, so unconditionally call
both.
| -rwxr-xr-x | debian/rules | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/debian/rules b/debian/rules index d39b8c6..71a7a31 100755 --- a/debian/rules +++ b/debian/rules @@ -8,10 +8,8 @@ include /usr/share/ocaml/ocamlvars.mk export VERBOSE := 1 TARGET := byte -INSTALL_TARGET := install-byte ifeq ($(OCAML_NATDYNLINK),yes) TARGET += opt - INSTALL_TARGET += install else export OPT := -byte endif @@ -30,7 +28,7 @@ override_dh_auto_build: .PHONY: override_dh_auto_install override_dh_auto_install: - $(MAKE) -f Makefile.coq $(INSTALL_TARGET) DSTROOT=$(CURDIR)/debian/tmp + $(MAKE) -f Makefile.coq install install-byte DSTROOT=$(CURDIR)/debian/tmp .PHONY: override_dh_install override_dh_install: |