max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(bin/lean-bootstrapped): remove obsolete file

Browse source
This commit is contained in:
Sebastian Ullrich 2019-05-24 11:05:49 +02:00
parent 074002eb84
commit 9d682d6465
1 changed files with 0 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
bin/lean-bootstrapped
View file

@ -1,19 +0,0 @@
#!/usr/bin/env bash
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)
echo "import init.lean.frontend #eval lean.process_file_json \"$@\"" | $leandir/bin/lean --stdin