From b1d00d9984b67da567c9fa6449a88a6d133a2e8a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 1 Apr 2021 17:57:16 +0200 Subject: [PATCH] fix: missing cmake dependency --- src/CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 308e0a442d..3ca8de84c3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -435,6 +435,8 @@ if(PREV_STAGE) configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make) add_custom_target(make_stdlib ALL WORKING_DIRECTORY ${LEAN_SOURCE_DIR} + # needed for linking `leanpkg` + DEPENDS leancpp # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server # for a parallelized nested build, but CMake doesn't let us do that. # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage