changeset 29145 | b1c6f4563df7 |
parent 28504 | 7ad7d7d6df47 |
child 31520 | 0a99c8716312 |
29144:ca186ebbd824 | 29145:b1c6f4563df7 |
---|---|
1 # -*- shell-script -*- :mode=shellscript: |
1 # -*- shell-script -*- :mode=shellscript: |
2 # $Id$ |
2 # |
3 # Author: Markus Wenzel, TU Muenchen |
3 # Author: Markus Wenzel, TU Muenchen |
4 # |
4 # |
5 # getsettings - bash source script to augment current env. |
5 # getsettings - bash source script to augment current env. |
6 |
6 |
7 if [ -z "$ISABELLE_SETTINGS_PRESENT" ] |
7 if [ -z "$ISABELLE_SETTINGS_PRESENT" ] |