equal
deleted
inserted
replaced
20 |
20 |
21 #users tend to put strange things in here ... |
21 #users tend to put strange things in here ... |
22 unset ENV |
22 unset ENV |
23 unset BASH_ENV |
23 unset BASH_ENV |
24 |
24 |
|
25 #support easy settings |
|
26 function choosefrom () |
|
27 { |
|
28 local RESULT="" |
|
29 local FILE="" |
|
30 |
|
31 for FILE in "$@" |
|
32 do |
|
33 [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE" |
|
34 done |
|
35 |
|
36 [ -z "$RESULT" ] && RESULT="$FILE" |
|
37 echo "$RESULT" |
|
38 } |
|
39 |
25 #get actual settings |
40 #get actual settings |
26 . $ISABELLE_HOME/etc/settings || exit 2 |
41 . $ISABELLE_HOME/etc/settings || exit 2 |
27 ISABELLE_SITE_SETTINGS_PRESENT=true |
42 ISABELLE_SITE_SETTINGS_PRESENT=true |
28 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings |
43 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings |
29 |
44 |