# HG changeset patch
# User wenzelm
# Date 967071233 -7200
# Node ID 6581bfc8421ee06ef031254e7da0dde33ee358da
# Parent  6dca83af209bd59a5260368fedc6ea26e5b50794
choosefrom: support easy settings;

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