equal
deleted
inserted
replaced
|
1 # |
|
2 # $Id$ |
|
3 # |
|
4 # patch-scripts.bash - relocate interpreter paths of Isabelle scripts. |
|
5 # |
|
6 |
|
7 ## find binaries |
|
8 |
|
9 function findbin() |
|
10 { |
|
11 local DEFAULT="$1" |
|
12 local BASE="" |
|
13 local BINARY="" |
|
14 |
|
15 if [ -f "$DEFAULT" ]; then # preferred location |
|
16 echo "found $DEFAULT" >&2 |
|
17 echo "$DEFAULT" |
|
18 return |
|
19 else # find in PATH |
|
20 BASE=$(basename "$DEFAULT") |
|
21 BINARY=$(type -path "$BASE") |
|
22 if [ -n "$BINARY" ]; then |
|
23 echo "found $BINARY" >&2 |
|
24 echo "$BINARY" |
|
25 return |
|
26 else |
|
27 echo "WARNING: $BASE not found!" >&2 |
|
28 echo "$DEFAULT" |
|
29 return |
|
30 fi |
|
31 fi |
|
32 } |
|
33 |
|
34 |
|
35 ## main |
|
36 |
|
37 BASH=$(findbin /bin/bash) |
|
38 PERL=$(findbin /usr/bin/perl) |
|
39 |
|
40 for FILE in $(find . -type f -print) |
|
41 do |
|
42 if [ -x "$FILE" ]; then |
|
43 sed -e "s:^#!.*/bash:#!$BASH:" -e "s:^#!.*/perl:#!$PERL:" $FILE >$FILE~~ |
|
44 if cmp $FILE $FILE~~ -s; then |
|
45 rm $FILE~~ |
|
46 else |
|
47 rm -f $FILE |
|
48 mv $FILE~~ $FILE |
|
49 chmod +x $FILE |
|
50 echo fixed $FILE |
|
51 fi |
|
52 fi |
|
53 done |