From 3b2bb854be2e65c500ad7433e10a67d8a2c69fc7 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 30 Nov 2016 20:33:42 -0500
Subject: [PATCH] fix(tests/lean/interactive/test_single): do not use
 deprecated realpath command

The realpath executable is not installed by default on ubuntu.  Also
contains a fix for macOS where the default readlink executable does not
understand -f.  The ./readlinkf.sh script does not work for directories
either.
---
 tests/lean/interactive/test_single.sh | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/tests/lean/interactive/test_single.sh b/tests/lean/interactive/test_single.sh
index 54b74043f6..16288a47ad 100755
--- a/tests/lean/interactive/test_single.sh
+++ b/tests/lean/interactive/test_single.sh
@@ -1,13 +1,17 @@
 #!/usr/bin/env bash
-REALPATH=realpath
-
 if [ $# -ne 3 -a $# -ne 2 ]; then
     echo "Usage: test_single.sh [lean-executable-path] [file] [yes/no]?"
     exit 1
 fi
 ulimit -s unlimited
 LEAN=$1
-ROOT_PATH=$($REALPATH ../../..)
+if command -v greadlink >/dev/null 2>&1; then
+  # macOS readlink doesn't support -f option
+  READLINK=greadlink
+else
+  READLINK=readlink
+fi
+ROOT_PATH=$($READLINK -f ../../..)
 
 if [[ "$OSTYPE" == "msys" ]]; then
     # Windows running MSYS2
@@ -16,7 +20,6 @@ if [[ "$OSTYPE" == "msys" ]]; then
 else
     ROOT_PATH_NORMALIZED=$ROOT_PATH
 fi
-
 export LEAN_PATH=$ROOT_PATH/library:.
 if [ $# -ne 3 ]; then
     INTERACTIVE=no