equal
deleted
inserted
replaced
1 # |
1 # -*- shell-script -*- |
2 # $Id$ |
2 # $Id$ |
3 # Author: Markus Wenzel, TU Muenchen |
3 # Author: Markus Wenzel, TU Muenchen |
4 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 # |
5 # |
6 # getsettings - bash source script to augment current env. |
6 # getsettings - bash source script to augment current env. |
14 ISABELLE_SETTINGS_PRESENT=true |
14 ISABELLE_SETTINGS_PRESENT=true |
15 |
15 |
16 #normalize ISABELLE_HOME as passed by caller |
16 #normalize ISABELLE_HOME as passed by caller |
17 ISABELLE_HOME=$(cd "$ISABELLE_HOME"; echo "$PWD") |
17 ISABELLE_HOME=$(cd "$ISABELLE_HOME"; echo "$PWD") |
18 |
18 |
19 #main executables |
19 #key executables |
20 ISABELLE="$ISABELLE_HOME/bin/isabelle" |
20 ISABELLE="$ISABELLE_HOME/bin/isabelle-process" |
21 ISATOOL="$ISABELLE_HOME/bin/isatool" |
21 ISATOOL="$ISABELLE_HOME/bin/isatool" |
22 |
22 |
23 #users tend to put strange things in here ... |
23 #users tend to put strange things in here ... |
24 unset ENV |
24 unset ENV |
25 unset BASH_ENV |
25 unset BASH_ENV |