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

chore(shell/CMakeLists): reactivate Lean tests

Browse source
This commit is contained in:
Sebastian Ullrich 2019-02-01 16:12:18 +01:00
parent a8f668a3d2
commit 7dc4d4e5fa
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/shell/CMakeLists.txt
View file

@ -98,6 +98,8 @@ if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
# COMMAND bash "./timeout.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "1" "slow1.lean")
endif()
# LEAN TESTS
file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
FOREACH(T ${LEANTESTS})
if(NOT T MATCHES "\\.#")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
@ -107,6 +109,8 @@ FOREACH(T ${LEANTESTS})
endif()
ENDFOREACH(T)
# LEAN RUN TESTS
file(GLOB LEANRUNTESTS "${LEAN_SOURCE_DIR}/../tests/lean/run/*.lean")
FOREACH(T ${LEANRUNTESTS})
if(NOT T MATCHES "\\.#")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
@ -116,6 +120,8 @@ FOREACH(T ${LEANRUNTESTS})
endif()
ENDFOREACH(T)
# LEAN FAIL TESTS
file(GLOB LEANFAILTESTS "${LEAN_SOURCE_DIR}/../tests/lean/fail/*.lean")
FOREACH(T ${LEANFAILTESTS})
if(NOT T MATCHES "\\.#")
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)