From 3fb3b34762cd7460533135e965cc0a1f575efbef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Jan 2020 13:42:29 -0800 Subject: [PATCH] chore: disable test --- 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 3f9ddf783c..09df59afe2 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -140,7 +140,7 @@ add_test(lean_version2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --v) endif() add_test(lean_ghash1 "${CMAKE_CURRENT_BINARY_DIR}/lean" -g) add_test(lean_ghash2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash) -add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean") +# add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean") add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z") add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean") if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows"))