changeset 9680 | 6581bfc8421e |
parent 9227 | 298ae5f69b18 |
child 9789 | 7e5e6c47c0b5 |
--- a/lib/scripts/getsettings Thu Aug 24 00:53:23 2000 +0200 +++ b/lib/scripts/getsettings Thu Aug 24 00:53:53 2000 +0200 @@ -22,6 +22,21 @@ unset ENV unset BASH_ENV +#support easy settings +function choosefrom () +{ + local RESULT="" + local FILE="" + + for FILE in "$@" + do + [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE" + done + + [ -z "$RESULT" ] && RESULT="$FILE" + echo "$RESULT" +} + #get actual settings . $ISABELLE_HOME/etc/settings || exit 2 ISABELLE_SITE_SETTINGS_PRESENT=true