| author | hoelzl | 
| Tue, 05 May 2009 17:09:18 +0200 | |
| changeset 31099 | 03314c427b34 | 
| parent 29143 | 72c960b2b83e | 
| child 50132 | 180d086c30dd | 
| 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  | 
| 28650 | 13  | 
echo "Usage: isabelle $PRG [OPTIONS]"  | 
| 
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)"  | 
|
| 6417 | 18  | 
echo " -p DIR install standalone binaries in DIR"  | 
| 5403 | 19  | 
echo  | 
| 6417 | 20  | 
echo " Install Isabelle executables with absolute references to the current"  | 
21  | 
echo " distribution directory."  | 
|
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
22  | 
echo  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
23  | 
exit 1  | 
| 
 
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  | 
|
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
26  | 
function fail()  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
27  | 
{
 | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
28  | 
echo "$1" >&2  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
29  | 
exit 2  | 
| 
 
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  | 
|
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
32  | 
|
| 5403 | 33  | 
## process command line  | 
34  | 
||
35  | 
# options  | 
|
36  | 
||
| 6450 | 37  | 
NO_OPTS=true  | 
38  | 
||
| 5403 | 39  | 
DISTDIR="$ISABELLE_HOME"  | 
| 6417 | 40  | 
BINDIR=""  | 
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
41  | 
|
| 16653 | 42  | 
while getopts "d:p:" OPT  | 
| 5403 | 43  | 
do  | 
| 15856 | 44  | 
NO_OPTS=""  | 
| 5403 | 45  | 
case "$OPT" in  | 
| 5404 | 46  | 
d)  | 
| 5403 | 47  | 
DISTDIR="$OPTARG"  | 
48  | 
;;  | 
|
| 6417 | 49  | 
p)  | 
50  | 
BINDIR="$OPTARG"  | 
|
| 15733 | 51  | 
;;  | 
| 5403 | 52  | 
\?)  | 
53  | 
usage  | 
|
54  | 
;;  | 
|
55  | 
esac  | 
|
56  | 
done  | 
|
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
57  | 
|
| 5403 | 58  | 
shift $(($OPTIND - 1))  | 
59  | 
||
60  | 
||
61  | 
# args  | 
|
62  | 
||
| 9788 | 63  | 
[ "$#" -ne 0 -o -n "$NO_OPTS" ] && usage  | 
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
64  | 
|
| 
15848
 
3001067227af
restored AUTO_BASH/PERL -- beware of ./configure!
 
wenzelm 
parents: 
15733 
diff
changeset
 | 
65  | 
|
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
66  | 
## main  | 
| 
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
67  | 
|
| 6459 | 68  | 
echo "referring to distribution at $DISTDIR"  | 
| 6417 | 69  | 
|
70  | 
||
71  | 
# standalone binaries  | 
|
| 
5362
 
29ce4f1fe72c
install binaries with absolute references to ISABELLE_HOME/bin;
 
wenzelm 
parents:  
diff
changeset
 | 
72  | 
|
| 6417 | 73  | 
if [ -n "$BINDIR" ]; then  | 
74  | 
mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"  | 
|
75  | 
||
| 
28915
 
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
 
wenzelm 
parents: 
28650 
diff
changeset
 | 
76  | 
for NAME in isabelle isabelle-process  | 
| 6417 | 77  | 
do  | 
78  | 
BIN="$BINDIR/$NAME"  | 
|
| 15856 | 79  | 
DIST="$DISTDIR/bin/$NAME"  | 
| 6417 | 80  | 
echo "installing $BIN"  | 
| 
15848
 
3001067227af
restored AUTO_BASH/PERL -- beware of ./configure!
 
wenzelm 
parents: 
15733 
diff
changeset
 | 
81  | 
rm -f "$BIN"  | 
| 26577 | 82  | 
echo "#!/usr/bin/env bash" > "$BIN" || fail "Cannot write file: $BIN"  | 
| 9788 | 83  | 
echo >> "$BIN"  | 
84  | 
echo "exec \"$DIST\" \"\$@\"" >> "$BIN"  | 
|
85  | 
chmod +x "$BIN"  | 
|
| 6417 | 86  | 
done  | 
87  | 
fi  |