patch-scripts.bash
author wenzelm
Mon, 16 Dec 1996 10:04:12 +0100
changeset 2407 f733d555b3d0
parent 2350 da4f8b250e1a
child 2475 36bdba95e170
permissions -rw-r--r--
added write_charnames';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2350
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
     1
#
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
     2
# $Id$
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
     3
#
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
     4
# patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
     5
#
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
     6
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
     7
## find binaries
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
     8
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
     9
function findbin()
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    10
{
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    11
  local DEFAULT="$1"
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    12
  local BASE=""
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    13
  local BINARY=""
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    14
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    15
  if [ -f "$DEFAULT" ]; then	# preferred location
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    16
    echo "found $DEFAULT" >&2
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    17
    echo "$DEFAULT"
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    18
    return
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    19
  else				# find in PATH
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    20
    BASE=$(basename "$DEFAULT")
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    21
    BINARY=$(type -path "$BASE")
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    22
    if [ -n "$BINARY" ]; then
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    23
      echo "found $BINARY" >&2
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    24
      echo "$BINARY"
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    25
      return
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    26
    else
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    27
      echo "WARNING: $BASE not found!" >&2
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    28
      echo "$DEFAULT"
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    29
      return
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    30
    fi
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    31
  fi
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    32
}
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    33
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    34
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    35
## main
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    36
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    37
BASH=$(findbin /bin/bash)
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    38
PERL=$(findbin /usr/bin/perl)
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    39
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    40
for FILE in $(find . -type f -print)
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    41
do
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    42
  if [ -x "$FILE" ]; then
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    43
    sed -e "s:^#!.*/bash:#!$BASH:" -e "s:^#!.*/perl:#!$PERL:" $FILE >$FILE~~
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    44
    if cmp $FILE $FILE~~ -s; then
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    45
      rm $FILE~~
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    46
    else
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    47
      rm -f $FILE
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    48
      mv $FILE~~ $FILE
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    49
      chmod +x $FILE
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    50
      echo fixed $FILE
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    51
    fi
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    52
  fi
da4f8b250e1a patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm
parents:
diff changeset
    53
done