patch-scripts.bash
author paulson
Fri Jan 03 15:01:55 1997 +0100 (1997-01-03)
changeset 2469 b50b8c0eec01
parent 2350 da4f8b250e1a
child 2475 36bdba95e170
permissions -rw-r--r--
Implicit simpsets and clasets for FOL and ZF
wenzelm@2350
     1
#
wenzelm@2350
     2
# $Id$
wenzelm@2350
     3
#
wenzelm@2350
     4
# patch-scripts.bash - relocate interpreter paths of Isabelle scripts.
wenzelm@2350
     5
#
wenzelm@2350
     6
wenzelm@2350
     7
## find binaries
wenzelm@2350
     8
wenzelm@2350
     9
function findbin()
wenzelm@2350
    10
{
wenzelm@2350
    11
  local DEFAULT="$1"
wenzelm@2350
    12
  local BASE=""
wenzelm@2350
    13
  local BINARY=""
wenzelm@2350
    14
wenzelm@2350
    15
  if [ -f "$DEFAULT" ]; then	# preferred location
wenzelm@2350
    16
    echo "found $DEFAULT" >&2
wenzelm@2350
    17
    echo "$DEFAULT"
wenzelm@2350
    18
    return
wenzelm@2350
    19
  else				# find in PATH
wenzelm@2350
    20
    BASE=$(basename "$DEFAULT")
wenzelm@2350
    21
    BINARY=$(type -path "$BASE")
wenzelm@2350
    22
    if [ -n "$BINARY" ]; then
wenzelm@2350
    23
      echo "found $BINARY" >&2
wenzelm@2350
    24
      echo "$BINARY"
wenzelm@2350
    25
      return
wenzelm@2350
    26
    else
wenzelm@2350
    27
      echo "WARNING: $BASE not found!" >&2
wenzelm@2350
    28
      echo "$DEFAULT"
wenzelm@2350
    29
      return
wenzelm@2350
    30
    fi
wenzelm@2350
    31
  fi
wenzelm@2350
    32
}
wenzelm@2350
    33
wenzelm@2350
    34
wenzelm@2350
    35
## main
wenzelm@2350
    36
wenzelm@2350
    37
BASH=$(findbin /bin/bash)
wenzelm@2350
    38
PERL=$(findbin /usr/bin/perl)
wenzelm@2350
    39
wenzelm@2350
    40
for FILE in $(find . -type f -print)
wenzelm@2350
    41
do
wenzelm@2350
    42
  if [ -x "$FILE" ]; then
wenzelm@2350
    43
    sed -e "s:^#!.*/bash:#!$BASH:" -e "s:^#!.*/perl:#!$PERL:" $FILE >$FILE~~
wenzelm@2350
    44
    if cmp $FILE $FILE~~ -s; then
wenzelm@2350
    45
      rm $FILE~~
wenzelm@2350
    46
    else
wenzelm@2350
    47
      rm -f $FILE
wenzelm@2350
    48
      mv $FILE~~ $FILE
wenzelm@2350
    49
      chmod +x $FILE
wenzelm@2350
    50
      echo fixed $FILE
wenzelm@2350
    51
    fi
wenzelm@2350
    52
  fi
wenzelm@2350
    53
done