Skip to content

Commit 614e612

Browse files
authored
chore: fix LEAN_PATH for building stage2+ Leanc.lean (#8705)
It would accidentally fall back to stage 1 otherwise
1 parent 1a9de50 commit 614e612

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/stdlib.make.in

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ Lean: Std
6262

6363
Leanc: Lean
6464
ifneq "${STAGE}" "0"
65-
+"${LEAN_BIN}/leanmake" -C "${CMAKE_BINARY_DIR}/leanc" lib PKG=Leanc $(LEANMAKE_OPTS) OUT="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}" LIB_OUT="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}"
65+
+"${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}"
6666
endif
6767

6868
Lake:
@@ -151,7 +151,7 @@ ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_D
151151

152152
lean: ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}
153153

154-
${CMAKE_BINARY_DIR}/bin/leanc${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLeanc.a
154+
${CMAKE_BINARY_DIR}/bin/leanc${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libLeanc.a
155155
@echo "[ ] Building $@"
156156
# on Windows, must remove file before writing a new one (since the old one may be in use)
157157
@rm -f $@

0 commit comments

Comments
 (0)