Skip to content

Commit 5920be2

Browse files
committed
chore: fix LEAN_PATH for stage2+ Leanc.lean
1 parent 6ba56a5 commit 5920be2

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/stdlib.make.in

Lines changed: 1 addition & 1 deletion
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_LIBRARY_OUTPUT_DIRECTORY}" LIB_OUT="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}" OLEAN_OUT="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}"
6666
endif
6767

6868
Lake:

0 commit comments

Comments
 (0)