From 6efd625825088a0f5645dab29787d8ae7cc48001 Mon Sep 17 00:00:00 2001 From: =?utf8?q?St=C3=A9phane=20Glondu?= Date: Wed, 19 Jun 2024 14:57:39 +0200 Subject: [PATCH] Do no longer call "make bootstrap" This implied building everything twice. Bootstrap is tested in upstream CI nowadays, and we don't make changes in the Debian package needing bootstrap. Even if we did, the procedure is rather complex and it is probably more reasonable to do it outside of the Debian package build process. --- debian/rules | 1 - 1 file changed, 1 deletion(-) diff --git a/debian/rules b/debian/rules index 90759125..c18dc457 100755 --- a/debian/rules +++ b/debian/rules @@ -143,7 +143,6 @@ build-stamp: config-stamp fi ifeq ($(BUILDCACHE),) $(MAKE) world - $(MAKE) bootstrap $(MAKE) -C tools dumpobj ifneq (,$(OCAML_OPT_ARCH)) @echo "Building native compilers" -- 2.30.2