michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(shell): remove obsolete tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-23 18:12:19 -07:00
parent 06da0ebaaf
commit eb794f7491
1 changed files with 0 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/shell/CMakeLists.txt
View file

@ -29,15 +29,6 @@ add_test(lean_unknown_option ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_
add_test(lean_unknown_file1 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
add_test(lean_unknown_file2 ${LEAN_SOURCE_DIR}/cmake/check_failure.sh "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lua")
# LEAN EXAMPLES
file(GLOB LEANEXAMPLES "${LEAN_SOURCE_DIR}/../examples/standard/*.lean")
FOREACH(T ${LEANEXAMPLES})
GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
add_test(NAME "leanex_${T_NAME}"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../examples/standard"
COMMAND ${LEAN_SOURCE_DIR}/shell/test_standard.sh ${CMAKE_CURRENT_BINARY_DIR}/lean ${T})
ENDFOREACH(T)
# LEAN TESTS
file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
FOREACH(T ${LEANTESTS})