max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: reenable test

Browse source 
/cc @leodemoura
This commit is contained in:
Sebastian Ullrich 2019-12-14 12:08:52 +01:00
parent 869b133b59
commit f183ea6fae
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/shell/CMakeLists.txt
View file

@ -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"))