| #!/usr/bin/env bash | |
| unamestr=`uname` | |
| if [[ "$unamestr" == 'Darwin' ]]; then | |
| # OSX | |
| if command -v greadlink >/dev/null 2>&1; then | |
| # macOS readlink doesn't support -f option | |
| READLINK=greadlink | |
| else | |
| echo "OSX 'readlink' command does not support option '-f', please install 'greadlink'. If you use 'brew', you can install 'greadlink' using 'brew install coreutils'" | |
| exit 1 | |
| fi | |
| else | |
| READLINK=readlink | |
| fi | |
| leandir=$(dirname $($READLINK -f $0))/.. | |
| leandir=$($READLINK -f $leandir) | |
| librarydir="$leandir/lib/lean" | |
| test -d "$librarydir" || librarydir="$leandir" | |
| LEAN_PATH=$librarydir/library:$librarydir/leanpkg \ | |
| PATH=$leandir/bin:$PATH \ | |
| exec lean --run $librarydir/leanpkg/leanpkg/main.lean "$@" |