From 9d682d64659f5ea32daea77df897316ce559f4b2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 24 May 2019 11:05:49 +0200
Subject: [PATCH] chore(bin/lean-bootstrapped): remove obsolete file

---
 bin/lean-bootstrapped | 19 -------------------
 1 file changed, 19 deletions(-)
 delete mode 100755 bin/lean-bootstrapped

diff --git a/bin/lean-bootstrapped b/bin/lean-bootstrapped
deleted file mode 100755
index 2316e95cf5..0000000000
--- a/bin/lean-bootstrapped
+++ /dev/null
@@ -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