From 45b505e808e73ef35223ce69e757189ca4df58ed Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Oct 2018 10:04:57 -0700 Subject: [PATCH] fix(CMakeLists): OSX build using `make` --- src/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1779bcd9ad..8e7ffd8342 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -467,7 +467,7 @@ endif () add_custom_target( standard_lib ALL - COMMAND make -j4 -e LEAN="${LEAN_SOURCE_DIR}/../bin/lean" "${LEAN_EXTRA_MAKE_OPTS}" + COMMAND make -j4 -e "LEAN=${LEAN_SOURCE_DIR}/../bin/lean ${LEAN_EXTRA_MAKE_OPTS}" DEPENDS bin_lean WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../library" )