lib/scripts/getsettings
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