diff -r 60d8d06f84a5 -r 024654b75919 patch-scripts.bash
--- a/patch-scripts.bash	Mon Feb 17 17:22:50 1997 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-#
-# $Id$
-#
-# patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
-#
-
-## find binaries
-
-function findbin()
-{
-  local DEFAULT="$1"
-  local BASE=""
-  local BINARY=""
-
-  if [ -f "$DEFAULT" ]; then	# preferred location
-    echo "found $DEFAULT" >&2
-    echo "$DEFAULT"
-    return
-  else				# find in PATH
-    BASE=$(basename "$DEFAULT")
-    BINARY=$(type -path "$BASE")
-    if [ -n "$BINARY" ]; then
-      echo "found $BINARY" >&2
-      echo "$BINARY"
-      return
-    else
-      echo "WARNING: $BASE not found!" >&2
-      echo "$DEFAULT"
-      return
-    fi
-  fi
-}
-
-
-## main
-
-BASH=$(findbin /bin/bash)
-PERL=$(findbin /usr/bin/perl)
-
-for FILE in $(find . -type f -print)
-do
-  if [ -x "$FILE" ]; then
-    sed -e "s:^#!.*/bash:#!$BASH:" -e "s:^#!.*/perl:#!$PERL:" $FILE >$FILE~~
-    if cmp -s $FILE $FILE~~; then
-      rm $FILE~~
-    else
-      rm -f $FILE
-      mv $FILE~~ $FILE
-      chmod +x $FILE
-      echo fixed $FILE
-    fi
-  fi
-done