From 614e6122f75cd6a1d553ac58c0a65ab47da40dc3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 10 Jun 2025 19:11:23 +0200 Subject: [PATCH] chore: fix `LEAN_PATH` for building stage2+ Leanc.lean (#8705) It would accidentally fall back to stage 1 otherwise --- src/stdlib.make.in | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/stdlib.make.in b/src/stdlib.make.in index c015fdf97b..1185d35780 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -62,7 +62,7 @@ Lean: Std Leanc: Lean ifneq "${STAGE}" "0" - +"${LEAN_BIN}/leanmake" -C "${CMAKE_BINARY_DIR}/leanc" lib PKG=Leanc $(LEANMAKE_OPTS) OUT="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}" LIB_OUT="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}" + +"${LEAN_BIN}/leanmake" -C "${CMAKE_BINARY_DIR}/leanc" lib PKG=Leanc $(LEANMAKE_OPTS) OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" LIB_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" OLEAN_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" endif Lake: @@ -151,7 +151,7 @@ ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_D lean: ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX} -${CMAKE_BINARY_DIR}/bin/leanc${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLeanc.a +${CMAKE_BINARY_DIR}/bin/leanc${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libLeanc.a @echo "[ ] Building $@" # on Windows, must remove file before writing a new one (since the old one may be in use) @rm -f $@