chore(tests/compiler/test.sh): rename to conventional test_single.sh so that (lean4-diff-test-file) works

2019-02-15 14:35:34 +01:00 · 2019-02-15 14:35:34 +01:00 · b8900fad80
commit b8900fad80
parent 00b177ad54
2 changed files with 1 additions and 1 deletions
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@ -144,7 +144,7 @@ FOREACH(T ${LEANCOMPTESTS})
  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
  add_test(NAME "leancomptest_${T_NAME}"
           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
-           COMMAND bash "./test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
+           COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
 ENDFOREACH(T)

 # LEANPKG TESTS
--- a/tests/compiler/test_single.sh
+++ b/tests/compiler/test_single.sh