From cf28981f458521c2beef3b6418248a5873c78110 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Jun 2014 07:47:46 -0700
Subject: [PATCH] feat(tests/lean/run): add test_single script that sets the
 LEAN_PATH

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/shell/CMakeLists.txt      |  2 +-
 tests/lean/run/test_single.sh | 16 ++++++++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100755 tests/lean/run/test_single.sh

diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 9d5835fa6..82df9785b 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -46,7 +46,7 @@ FOREACH(T ${LEANRUNTESTS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
   add_test(NAME "leanruntest_${T_NAME}"
            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run"
-           COMMAND "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
+           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
 ENDFOREACH(T)
 
 # LEAN INTERACTIVE TESTS
diff --git a/tests/lean/run/test_single.sh b/tests/lean/run/test_single.sh
new file mode 100755
index 000000000..4e1e6e05c
--- /dev/null
+++ b/tests/lean/run/test_single.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+if [ $# -ne 2 ]; then
+    echo "Usage: test_single.sh [lean-executable-path] [file]"
+    exit 1
+fi
+ulimit -s 8192
+LEAN=$1
+export LEAN_PATH=../../../library/standard:.
+f=$2
+echo "-- testing $f"
+if $LEAN $f; then
+   echo "-- checked"
+else
+   echo "failed $f"
+   exit 1
+fi