# HG changeset patch
# User wenzelm
# Date 850146431 -3600
# Node ID da4f8b250e1aae296fe8be509b3eb0649ac723fd
# Parent  e9475a7be4add5ca64d9ac1f0ef625596f3472a0
patch-scripts.bash - relocate interpreter paths of Isabelle scripts.

diff -r e9475a7be4ad -r da4f8b250e1a patch-scripts.bash
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/patch-scripts.bash	Mon Dec 09 16:47:11 1996 +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 $FILE $FILE~~ -s; then
+      rm $FILE~~
+    else
+      rm -f $FILE
+      mv $FILE~~ $FILE
+      chmod +x $FILE
+      echo fixed $FILE
+    fi
+  fi
+done