diff options
Diffstat (limited to 'debian/rules')
| -rwxr-xr-x | debian/rules | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules index 8c97cf17..db2ddc0f 100755 --- a/debian/rules +++ b/debian/rules @@ -65,7 +65,10 @@ ifeq ($(BUILDCACHE),) # the default one without -silent (-silent maybe cause buildd to # timeout because of lack of output) +# Don't combine `make world` and `make byte`--doing so triggers a race +# in the build system. See upstream's CHANGES. $(MAKE) world STRIP=true + $(MAKE) byte STRIP=true $(MAKE) DOC_TARGETS=$(HTMLDOC) $(HTMLDOC) else rsync -a --exclude=debian --exclude=.git $(BUILDCACHE)/ . @@ -84,7 +87,7 @@ override_dh_auto_test: .PHONY: override_dh_auto_install override_dh_auto_install: - $(MAKE) $(ADDPREF) install + $(MAKE) $(ADDPREF) install install-byte find debian/tmp -regextype posix-awk \ -regex '.*\.(cmi|cmx|cmxa|[ao])$$' \ | grep -v toploop/ | grep -v coq-native \ |