changeset 25650 | ce061f5083d7 |
parent 25434 | 746677c843a7 |
child 27908 | 97f8b7c0f420 |
--- a/lib/scripts/getsettings Sat Dec 15 20:10:26 2007 +0100 +++ b/lib/scripts/getsettings Sat Dec 15 21:17:48 2007 +0100 @@ -44,6 +44,13 @@ echo "$RESULT" } +#Java path wrapper +if [ "$OSTYPE" = cygwin ]; then + function javapath() { cygpath -w "$@"; } +else + function javapath() { echo "$@"; } +fi + #get actual settings source "$ISABELLE_HOME/etc/settings" || exit 2 ISABELLE_SITE_SETTINGS_PRESENT=true