From ad3ac150bcc357d13d868b97c0df6282c911da40 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 22 Apr 2025 18:03:12 +0200 Subject: [PATCH] chore: remove lakefile copy in root and tests/ (#8054) As we use a different Lean in these directories, using those copies always results in a full rebuild --- src/CMakeLists.txt | 2 -- src/stdlib.make.in | 2 +- 2 files changed, 1 insertion(+), 3 deletions(-) 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