diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2e1498d9b8..d03af695ca 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -843,6 +843,4 @@ endif() if(USE_LAKE AND STAGE EQUAL 1) configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml) - configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../tests/lakefile.toml) - configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../lakefile.toml) endif() diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 659f08c2ff..f3a5086e3b 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -41,7 +41,7 @@ ifeq "${USE_LAKE} ${STAGE}" "ON 1" # build in parallel Init: - ${PREV_STAGE}/bin/lake build Init Std Lean Lake LakeMain + ${PREV_STAGE}/bin/lake build Init Std Lean Lake LakeMain $(LAKE_EXTRA_ARGS) Std Lean Lake: Init