1 files changed, 0 insertions, 54 deletions
diff --git a/math/isabelle/files/patch-lib-Tools-install b/math/isabelle/files/patch-lib-Tools-install
deleted file mode 100644
index 8c61bcea857e..000000000000
--- a/math/isabelle/files/patch-lib-Tools-install
+++ /dev/null
@@ -1,54 +0,0 @@
---- ./lib/Tools/install.orig	Sun Sep  2 15:11:55 2007
-+++ ./lib/Tools/install	Sun Sep  2 15:52:30 2007
-@@ -1,4 +1,4 @@
--#!/usr/bin/env bash
-+#!/bin/sh
- #
- # $Id: install,v 1.25 2005/07/01 12:41:57 wenzelm Exp $
- # Author: Markus Wenzel, TU Muenchen
-@@ -8,7 +8,7 @@
- 
- PRG=$(basename "$0")
- 
--function usage()
-+usage()
- {
-   echo
-   echo "Usage: $PRG [OPTIONS]"
-@@ -24,7 +24,7 @@
-   exit 1
- }
- 
--function fail()
-+fail()
- {
-   echo "$1" >&2
-   exit 2
-@@ -71,18 +71,6 @@
- 
- # standalone binaries
- 
--#set by configure
--AUTO_BASH=bash
--
--case "$AUTO_BASH" in
--  /*)
--    BASH="$AUTO_BASH"
--    ;;
--  *)
--    BASH="/usr/bin/env bash"
--    ;;
--esac
--
- if [ -n "$BINDIR" ]; then
-   mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"
- 
-@@ -92,7 +80,7 @@
-     DIST="$DISTDIR/bin/$NAME"
-     echo "installing $BIN"
-     rm -f "$BIN"
--    echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN"
-+    echo "#!/bin/sh" > "$BIN" || fail "Cannot write file: $BIN"
-     echo >> "$BIN"
-     echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
-     chmod +x "$BIN"