lib/scripts/patch-scripts.bash
author wenzelm
Tue, 13 Feb 2001 16:31:18 +0100
changeset 11109 ce1cefc6c14c
parent 10512 d34192966cd8
child 14981 e73f8140af78
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10512
wenzelm
parents: 9789
diff changeset
     1
# -*- shell-script -*-
2651
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
     2
# $Id$
9789
wenzelm
parents: 6974
diff changeset
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm
parents: 6974
diff changeset
     4
# License: GPL (GNU GENERAL PUBLIC LICENSE)
2651
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
     5
#
6974
60b0e4bbe331 may get BASH_PATH etc. from env;
wenzelm
parents: 6105
diff changeset
     6
# patch-scripts.bash - relocate interpreter paths of executable scripts and
60b0e4bbe331 may get BASH_PATH etc. from env;
wenzelm
parents: 6105
diff changeset
     7
#   insert AUTO_BASH/AUTO_PERL values
2651
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
     8
#
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
     9
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    10
## find binaries
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    11
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    12
function findbin()
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    13
{
6974
60b0e4bbe331 may get BASH_PATH etc. from env;
wenzelm
parents: 6105
diff changeset
    14
  local BASE="$1"
2651
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    15
  local BINARY=""
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    16
3052
b7922b9d7acd no longer forces default;
wenzelm
parents: 2760
diff changeset
    17
  BINARY=$(type -path "$BASE")
b7922b9d7acd no longer forces default;
wenzelm
parents: 2760
diff changeset
    18
b7922b9d7acd no longer forces default;
wenzelm
parents: 2760
diff changeset
    19
  if [ -n "$BINARY" ]; then
6974
60b0e4bbe331 may get BASH_PATH etc. from env;
wenzelm
parents: 6105
diff changeset
    20
    echo "found $BINARY" >&2
3052
b7922b9d7acd no longer forces default;
wenzelm
parents: 2760
diff changeset
    21
    echo "$BINARY"
b7922b9d7acd no longer forces default;
wenzelm
parents: 2760
diff changeset
    22
    return
b7922b9d7acd no longer forces default;
wenzelm
parents: 2760
diff changeset
    23
  else
4508
f102cb0140fe do require perl;
wenzelm
parents: 3052
diff changeset
    24
    echo "ERROR: $BASE not found!" >&2
3052
b7922b9d7acd no longer forces default;
wenzelm
parents: 2760
diff changeset
    25
    echo "$DEFAULT"
b7922b9d7acd no longer forces default;
wenzelm
parents: 2760
diff changeset
    26
    return
2651
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    27
  fi
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    28
}
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    29
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    30
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    31
## main
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    32
6974
60b0e4bbe331 may get BASH_PATH etc. from env;
wenzelm
parents: 6105
diff changeset
    33
[ -z "$BASH_PATH" ] && BASH_PATH=$(findbin bash)
60b0e4bbe331 may get BASH_PATH etc. from env;
wenzelm
parents: 6105
diff changeset
    34
[ -z "$PERL_PATH" ] && PERL_PATH=$(findbin perl)
60b0e4bbe331 may get BASH_PATH etc. from env;
wenzelm
parents: 6105
diff changeset
    35
[ -z "$AUTO_BASH" ] && AUTO_BASH="$BASH_PATH"
60b0e4bbe331 may get BASH_PATH etc. from env;
wenzelm
parents: 6105
diff changeset
    36
[ -z "$AUTO_PERL" ] && AUTO_PERL="$PERL_PATH"
2651
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    37
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    38
for FILE in $(find . -type f -print)
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    39
do
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    40
  if [ -x "$FILE" ]; then
6974
60b0e4bbe331 may get BASH_PATH etc. from env;
wenzelm
parents: 6105
diff changeset
    41
    sed -e "s:^#!.*/bash:#!$BASH_PATH:" -e "s:^#!.*/perl:#!$PERL_PATH:" \
60b0e4bbe331 may get BASH_PATH etc. from env;
wenzelm
parents: 6105
diff changeset
    42
      -e "s:^AUTO_BASH=.*bash:AUTO_BASH=$AUTO_BASH:" \
9789
wenzelm
parents: 6974
diff changeset
    43
      -e "s:^AUTO_PERL=.*perl:AUTO_PERL=$AUTO_PERL:" "$FILE" > "$FILE~~"
wenzelm
parents: 6974
diff changeset
    44
    if cmp -s "$FILE" "$FILE~~"; then
wenzelm
parents: 6974
diff changeset
    45
      rm "$FILE~~"
2651
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    46
    else
9789
wenzelm
parents: 6974
diff changeset
    47
      rm -f "$FILE"
wenzelm
parents: 6974
diff changeset
    48
      mv "$FILE~~" "$FILE"
wenzelm
parents: 6974
diff changeset
    49
      chmod +x "$FILE"
wenzelm
parents: 6974
diff changeset
    50
      echo "fixed $FILE"
2651
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    51
    fi
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    52
  fi
60d8d06f84a5 file moved here;
wenzelm
parents:
diff changeset
    53
done