| author | blanchet | 
| Mon, 07 Aug 2017 10:59:49 +0200 | |
| changeset 66362 | 9b70e98490da | 
| parent 63995 | 2e4d80723fb0 | 
| child 79059 | ae682b2aab03 | 
| permissions | -rwxr-xr-x | 
| 10555 | 1  | 
#!/usr/bin/env bash  | 
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
2  | 
#  | 
| 9788 | 3  | 
# Author: Markus Wenzel, TU Muenchen  | 
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
4  | 
#  | 
| 6417 | 5  | 
# DESCRIPTION: install standalone Isabelle executables  | 
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
6  | 
|
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
7  | 
|
| 9788 | 8  | 
PRG=$(basename "$0")  | 
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
9  | 
|
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
10  | 
function usage()  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
11  | 
{
 | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
12  | 
echo  | 
| 50132 | 13  | 
echo "Usage: isabelle $PRG [OPTIONS] BINDIR"  | 
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
14  | 
echo  | 
| 5403 | 15  | 
echo " Options are:"  | 
| 7887 | 16  | 
echo " -d DISTDIR refer to DISTDIR as Isabelle distribution"  | 
17  | 
echo " (default ISABELLE_HOME)"  | 
|
| 5403 | 18  | 
echo  | 
| 50132 | 19  | 
echo " Install Isabelle executables with absolute references to the"  | 
| 6417 | 20  | 
echo " distribution directory."  | 
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
21  | 
echo  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
22  | 
exit 1  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
23  | 
}  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
24  | 
|
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
25  | 
function fail()  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
26  | 
{
 | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
27  | 
echo "$1" >&2  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
28  | 
exit 2  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
29  | 
}  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
30  | 
|
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
31  | 
|
| 5403 | 32  | 
## process command line  | 
33  | 
||
34  | 
# options  | 
|
35  | 
||
36  | 
DISTDIR="$ISABELLE_HOME"  | 
|
| 6417 | 37  | 
BINDIR=""  | 
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
38  | 
|
| 50132 | 39  | 
while getopts "d:" OPT  | 
| 5403 | 40  | 
do  | 
41  | 
case "$OPT" in  | 
|
| 5404 | 42  | 
d)  | 
| 5403 | 43  | 
DISTDIR="$OPTARG"  | 
44  | 
;;  | 
|
45  | 
\?)  | 
|
46  | 
usage  | 
|
47  | 
;;  | 
|
48  | 
esac  | 
|
49  | 
done  | 
|
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
50  | 
|
| 5403 | 51  | 
shift $(($OPTIND - 1))  | 
52  | 
||
53  | 
||
54  | 
# args  | 
|
55  | 
||
| 50132 | 56  | 
[ "$#" -ge 1 ] && { BINDIR="$1"; shift; }
 | 
57  | 
[ "$#" -ne 0 -o -z "$BINDIR" ] && usage  | 
|
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
58  | 
|
| 
15848
 
3001067227af
restored AUTO_BASH/PERL -- beware of ./configure!
 
wenzelm 
parents: 
15733 
diff
changeset
 | 
59  | 
|
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
60  | 
## main  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
61  | 
|
| 50132 | 62  | 
echo "referring to distribution at \"$DISTDIR\""  | 
| 6417 | 63  | 
|
| 50132 | 64  | 
mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""  | 
| 6417 | 65  | 
|
| 63995 | 66  | 
for NAME in isabelle isabelle_java isabelle_scala_script  | 
| 50132 | 67  | 
do  | 
68  | 
BIN="$BINDIR/$NAME"  | 
|
69  | 
DIST="$DISTDIR/bin/$NAME"  | 
|
70  | 
echo "installing $BIN"  | 
|
71  | 
rm -f "$BIN"  | 
|
72  | 
echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN"  | 
|
73  | 
echo >> "$BIN"  | 
|
74  | 
echo "exec \"$DIST\" \"\$@\"" >> "$BIN"  | 
|
75  | 
chmod +x "$BIN"  | 
|
76  | 
done  |