From 606c149cd6834fa3fa63b3f864329287984aefc5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 17 Mar 2026 11:28:51 +0100 Subject: [PATCH] chore: fix update-stage0 with make build (#12943) This PR fixes the stage0 build with -DUSE_LAKE=OFF --- src/stdlib.make.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/stdlib.make.in b/src/stdlib.make.in index e5dccb3e87..7acd183ef7 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -84,7 +84,7 @@ Lake: Lean +"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export PKG=Lake $(LEANMAKE_OPTS) OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" EXTRA_SRC_ROOTS=LakeMain.lean LeanChecker: Lake - +"${LEAN_BIN}/leanmake" lib PKG=LeanChecker $(LEANMAKE_OPTS) OUT="$(OUTARC)" LIB_OUT="$(OUTARC)" OLEAN_OUT="$(OUTARC)" + +"${LEAN_BIN}/leanmake" lib PKG=LeanChecker $(LEANMAKE_OPTS) OUT="$(OUTARC)" LIB_OUT="$(OUTARC)" TEMP_OUT="${LIB}/temp" OLEAN_OUT="$(OUTARC)" endif