equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 # DESCRIPTION: install binaries with absolute references to ISABELLE_HOME/bin |
5 # DESCRIPTION: install binaries with absolute references to distribution |
6 |
6 |
7 |
7 |
8 PRG=$(basename $0) |
8 PRG=$(basename $0) |
9 |
9 |
10 function usage() |
10 function usage() |
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: $PRG DIR" |
13 echo "Usage: $PRG BINDIR" |
14 echo |
14 echo |
15 echo " Install binaries in directory DIR with absolute references to" |
15 echo " Options are:" |
16 echo " $ISABELLE_HOME/bin (non-movable)." |
16 echo " -d DISTDIR use DISTDIR as Isabelle distribution (default ISABELLE_HOME)" |
|
17 echo |
|
18 echo " Install binaries in directory BINDIR with absolute references to" |
|
19 echo " DISTDIR/bin, which basically becomes non-relocatable this way." |
17 echo |
20 echo |
18 exit 1 |
21 exit 1 |
19 } |
22 } |
20 |
23 |
21 function fail() |
24 function fail() |
23 echo "$1" >&2 |
26 echo "$1" >&2 |
24 exit 2 |
27 exit 2 |
25 } |
28 } |
26 |
29 |
27 |
30 |
28 ## args |
31 ## process command line |
29 |
32 |
30 DIR="" |
33 # options |
31 [ $# -ge 1 ] && { DIR="$1"; shift; } |
|
32 |
34 |
33 [ $# -ne 0 -o -z "$DIR" -o "$DIR" = "-?" ] && usage |
35 DISTDIR="$ISABELLE_HOME" |
|
36 |
|
37 while getopts "d:" OPT |
|
38 do |
|
39 case "$OPT" in |
|
40 h) |
|
41 DISTDIR="$OPTARG" |
|
42 ;; |
|
43 \?) |
|
44 usage |
|
45 ;; |
|
46 esac |
|
47 done |
|
48 |
|
49 shift $(($OPTIND - 1)) |
|
50 |
|
51 |
|
52 # args |
|
53 |
|
54 BINDIR="" |
|
55 [ $# -ge 1 ] && { BINDIR="$1"; shift; } |
|
56 |
|
57 [ $# -ne 0 -o -z "$BINDIR" -o "$BINDIR" = "-?" ] && usage |
34 |
58 |
35 |
59 |
36 ## main |
60 ## main |
37 |
61 |
38 mkdir -p "$DIR" || fail "Bad directory: $DIR" |
62 mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR" |
39 |
63 |
40 BASH=$(type -path bash) |
64 BASH=$(type -path bash) |
41 [ -z "$BASH" ] && fail "Cannot find bash!" |
65 [ -z "$BASH" ] && fail "Cannot find bash!" |
42 |
66 |
43 for BIN in $ISABELLE_HOME/bin/* |
67 echo "using $DISTDIR" |
|
68 |
|
69 for NAME in isatool isabelle Isabelle |
44 do |
70 do |
45 if [ -f "$BIN" -a -x "$BIN" ]; then |
71 BIN="$BINDIR/$NAME" |
46 B=$DIR/$(basename $BIN) |
72 DIST="$DISTDIR/bin/$NAME" |
47 echo "install $B" |
73 echo "installing $BIN" |
48 echo "#!$BASH" >$B || fail "Cannot write file: $B" |
74 echo "#!$BASH" >$BIN || fail "Cannot write file: $BIN" |
49 echo >>$B |
75 echo >>$BIN |
50 echo "exec $BIN \"\$@\"" >>$B |
76 echo "exec $DIST \"\$@\"" >>$BIN |
51 chmod +x $B |
77 chmod +x $BIN |
52 fi |
|
53 done |
78 done |