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.

diff --git a/debian/rules b/debian/rules
index 90759125891064c923279d8abadda63e7acaf747..c18dc4574fd9bb6a35076d2fab65529e7f7222da 100755 (executable)
--- 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"