diff -r 6dca83af209b -r 6581bfc8421e lib/scripts/getsettings
--- 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