From 81ff285427a2c36d2146c9b60c898ca1ce963fa0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Aug 2021 08:52:04 -0700 Subject: [PATCH] chore: use `leanmake` instead of `leanpkg` --- src/shell/CMakeLists.txt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 17ed12d6d5..ee96d2e92c 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -186,7 +186,7 @@ add_test(NAME leanpkgtest_user_ext set -eu export PATH=${LEAN_BIN}:$PATH find . -name '*.olean' -delete - leanpkg build | grep 'world, hello, test'") + leanmake | grep 'world, hello, test'") add_test(NAME leanpkgtest_user_attr WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_attr" @@ -194,7 +194,7 @@ add_test(NAME leanpkgtest_user_attr set -eu export PATH=${LEAN_BIN}:$PATH find . -name '*.olean' -delete - leanpkg build") + leanmake") add_test(NAME leanpkgtest_user_opt WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_opt" @@ -202,7 +202,7 @@ add_test(NAME leanpkgtest_user_opt set -eu export PATH=${LEAN_BIN}:$PATH find . -name '*.olean' -delete - leanpkg build") + leanmake") add_test(NAME leanpkgtest_prv WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/prv" @@ -210,4 +210,4 @@ add_test(NAME leanpkgtest_prv set -eu export PATH=${LEAN_BIN}:$PATH find . -name '*.olean' -delete - leanpkg build 2>&1 | grep 'error: field.*private'") + leanmake 2>&1 | grep 'error: field.*private'")