Skip to content

Commit

Permalink
chore: build Lean with Elab.async (#6989)
Browse files Browse the repository at this point in the history
  • Loading branch information
Kha committed Feb 11, 2025
1 parent ce5994c commit f568974
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/stdlib.make.in
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ LEANMAKE_OPTS=\
LIB_OUT="${LIB}/lean"\
OLEAN_OUT="${LIB}/lean"\
BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS}"\
LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -DElab.async=true"\
LEANC_OPTS+="${LEANC_OPTS}"\
LEAN_AR="${CMAKE_AR}"\
MORE_DEPS+="${PREV_STAGE}/bin/lean${PREV_STAGE_CMAKE_EXECUTABLE_SUFFIX}"\
Expand Down

0 comments on commit f568974

Please sign in to comment.