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.
This commit is contained in:
parent
7db2b8d014
commit
3b2bb854be
1 changed files with 7 additions and 4 deletions
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue