# HG changeset patch
# User wenzelm
# Date 856196570 -3600
# Node ID 60d8d06f84a5dcc97b0252e5b8afca20ce6ed3d1
# Parent  96234bf96bf96cf73ab3ec5b3dc206da477f58db
file moved here;

diff -r 96234bf96bf9 -r 60d8d06f84a5 lib/scripts/patch-scripts.bash
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/patch-scripts.bash	Mon Feb 17 17:22:50 1997 +0100
@@ -0,0 +1,53 @@
+#
+# $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