lib/scripts/getsettings
changeset 29145 b1c6f4563df7
parent 28504 7ad7d7d6df47
child 31520 0a99c8716312
equal deleted inserted replaced
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" ]