From b8900fad800b9ffb3316b0614c0b8851cf199b8b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 15 Feb 2019 14:35:34 +0100
Subject: [PATCH] chore(tests/compiler/test.sh): rename to conventional
 `test_single.sh` so that (lean4-diff-test-file) works

---
 src/shell/CMakeLists.txt                   | 2 +-
 tests/compiler/{test.sh => test_single.sh} | 0
 2 files changed, 1 insertion(+), 1 deletion(-)
 rename tests/compiler/{test.sh => test_single.sh} (100%)

diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 6e741f9c25..3b549a43ae 100644
--- 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
diff --git a/tests/compiler/test.sh b/tests/compiler/test_single.sh
similarity index 100%
rename from tests/compiler/test.sh
rename to tests/compiler/test_single.sh