From de5c7cbff04a0eb261bc446f7a0fc669b9b724a7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 9 Aug 2019 16:40:45 +0200 Subject: [PATCH] fix(shell/CMakeLists): bin_lean_stage0 should not be part of the default target as it conflicts with bin_lean /cc @leodemoura --- src/shell/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index b89c5769f4..bb5ce8bc04 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -6,7 +6,7 @@ else() set_target_properties(lean_stage0 PROPERTIES IMPORTED_LOCATION "${CMAKE_CURRENT_BINARY_DIR}/lean_stage0") endif() -ADD_CUSTOM_TARGET(bin_lean_stage0 ALL +ADD_CUSTOM_TARGET(bin_lean_stage0 COMMAND "${CMAKE_COMMAND}" -E copy_if_different "$" "${LEAN_SOURCE_DIR}/../bin/lean" DEPENDS lean_stage0 )