From b2f467abc0d2caaf40b6446a567f968ce935247f Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 21 May 2020 16:42:30 +0200
Subject: [PATCH] Improve -with-bootstrap mode

- coreboot + opt.opt gives a faster build than bootstrap + opt.opt
- Restore the original bootstrap compilers on exit, so that
  other-configs works (it performs several builds in sequence).
---
 tools/ci/inria/main | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/tools/ci/inria/main b/tools/ci/inria/main
index 4492c82ca..a121489ee 100755
--- a/tools/ci/inria/main
+++ b/tools/ci/inria/main
@@ -235,10 +235,11 @@ eval ./configure "$CCOMP" $build $host --prefix='$instdir' $confoptions
 
 if $bootstrap; then
   $make $jobs --warn-undefined-variables core
-  $make $jobs --warn-undefined-variables bootstrap
+  $make $jobs --warn-undefined-variables coreboot
   if $make_native; then
-    $make $jobs --warn-undefined-variables opt
     $make $jobs --warn-undefined-variables opt.opt
+  else
+    $make $jobs --warn-undefined-variables all
   fi
 else
   $make $jobs --warn-undefined-variables
@@ -264,3 +265,7 @@ if test -n "$jobs" && test -x /usr/bin/parallel
 then PARALLEL="$jobs $PARALLEL" $make --warn-undefined-variables parallel
 else $make --warn-undefined-variables all
 fi
+
+if $bootstrap; then
+  git checkout ../boot/ocamlc ../boot/ocamllex
+fi