equal
deleted
inserted
replaced
13 |
13 |
14 #users tend to put strange things in here ... |
14 #users tend to put strange things in here ... |
15 unset ENV |
15 unset ENV |
16 unset BASH_ENV |
16 unset BASH_ENV |
17 |
17 |
18 #get bash-style platform info -- has to work around some tricky features |
|
19 unset HOSTTYPE |
|
20 unset OSTYPE |
|
21 PLATFORM=$(bash -norc -c 'echo $HOSTTYPE-$OSTYPE') |
|
22 |
|
23 #get actual settings |
18 #get actual settings |
24 . $ISABELLE_HOME/etc/settings || exit 2 |
19 . $ISABELLE_HOME/etc/settings || exit 2 |
25 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings |
20 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings |
26 |
21 |
27 #derived values |
22 #derived values |
28 ISABELLE=$ISABELLE_HOME/bin/isabelle |
23 ISABELLE=$ISABELLE_HOME/bin/isabelle |
29 ISATOOL=$ISABELLE_HOME/bin/isatool |
24 ISATOOL=$ISABELLE_HOME/bin/isatool |
30 ISABELLE_OUTPUT_DIR="$ISABELLE_OUTPUT/$ML_SYSTEM-$PLATFORM" |
|
31 |
25 |
32 set +o allexport |
26 set +o allexport |