author | wenzelm |
Wed, 14 May 2008 11:05:10 +0200 | |
changeset 26882 | 9e824d8f4512 |
parent 25650 | ce061f5083d7 |
child 27908 | 97f8b7c0f420 |
permissions | -rw-r--r-- |
25434
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset
|
1 |
# -*- shell-script -*- :mode=shellscript: |
2307 | 2 |
# $Id$ |
9789 | 3 |
# Author: Markus Wenzel, TU Muenchen |
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
4 |
# |
2348 | 5 |
# getsettings - bash source script to augment current env. |
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
6 |
|
7770
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
7 |
if [ -z "$ISABELLE_SETTINGS_PRESENT" ] |
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
8 |
then |
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
9 |
|
3185 | 10 |
set -o allexport |
11 |
||
7770
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
12 |
ISABELLE_SETTINGS_PRESENT=true |
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
13 |
|
15972 | 14 |
export ISABELLE_HOME |
12598 | 15 |
if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; } |
16 |
then |
|
17 |
echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!" |
|
18 |
echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\"" |
|
19 |
fi |
|
2736 | 20 |
|
11553 | 21 |
#key executables |
22 |
ISABELLE="$ISABELLE_HOME/bin/isabelle-process" |
|
9789 | 23 |
ISATOOL="$ISABELLE_HOME/bin/isatool" |
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
24 |
|
25434
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset
|
25 |
#Isabelle distribution identifier -- filled in automatically! |
746677c843a7
ISABELLE_IDENTIFIER is filled in automatically, not taken from the *long* form of isatool version!
wenzelm
parents:
21490
diff
changeset
|
26 |
ISABELLE_IDENTIFIER="" |
21490 | 27 |
|
2643 | 28 |
#users tend to put strange things in here ... |
2621 | 29 |
unset ENV |
30 |
unset BASH_ENV |
|
31 |
||
9680 | 32 |
#support easy settings |
33 |
function choosefrom () |
|
34 |
{ |
|
35 |
local RESULT="" |
|
36 |
local FILE="" |
|
37 |
||
38 |
for FILE in "$@" |
|
39 |
do |
|
40 |
[ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE" |
|
41 |
done |
|
42 |
||
43 |
[ -z "$RESULT" ] && RESULT="$FILE" |
|
44 |
echo "$RESULT" |
|
45 |
} |
|
46 |
||
25650 | 47 |
#Java path wrapper |
48 |
if [ "$OSTYPE" = cygwin ]; then |
|
49 |
function javapath() { cygpath -w "$@"; } |
|
50 |
else |
|
51 |
function javapath() { echo "$@"; } |
|
52 |
fi |
|
53 |
||
2643 | 54 |
#get actual settings |
15972 | 55 |
source "$ISABELLE_HOME/etc/settings" || exit 2 |
9227 | 56 |
ISABELLE_SITE_SETTINGS_PRESENT=true |
9789 | 57 |
|
58 |
[ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \ |
|
59 |
{ echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; } |
|
16253 | 60 |
[ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \ |
16293 | 61 |
{ source "$ISABELLE_HOME_USER/etc/settings" || exit 2; } |
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
62 |
|
21490 | 63 |
#ML system identifier |
6413 | 64 |
if [ -z "$ML_PLATFORM" ]; then |
65 |
ML_IDENTIFIER="$ML_SYSTEM" |
|
66 |
else |
|
67 |
ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
|
68 |
fi |
|
21468
c7892915ed10
add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;
wenzelm
parents:
16293
diff
changeset
|
69 |
|
6413 | 70 |
ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" |
3118 | 71 |
|
2299
ed9720047d53
getsettings: bash source script to augment current env.
wenzelm
parents:
diff
changeset
|
72 |
set +o allexport |
7770
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
73 |
|
0497323c1f0b
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
wenzelm
parents:
6413
diff
changeset
|
74 |
fi |