diff --git a/src/lakefile.toml.in b/src/lakefile.toml.in index a95ce9377c..73107ef31c 100644 --- a/src/lakefile.toml.in +++ b/src/lakefile.toml.in @@ -13,6 +13,11 @@ defaultTargets = ["Init", "Std", "Lean", "Lake", "LakeMain", "Leanc"] # The root of all the compiler output directories buildDir = "${CMAKE_BINARY_DIR}" +# Ensure build artifacts end up in the build directory even when the Lake +# local artifact cache is enabled. This is necessary because subsequent stages +# will expect the previous stage's artifacts to be in the build directory. +restoreAllArtifacts = true + # The directory of Lean source files (i.e., `src`) srcDir = "${LEAN_SOURCE_DIR}"