added jvmpath conversion for Cygwin;
authorwenzelm
Tue, 21 Oct 2008 23:52:17 +0200
changeset 34339 8c70469bc83a
parent 34338 b7fdb6b14e0b
child 34340 19160c63b4d1
added jvmpath conversion for Cygwin;
src/Tools/jEdit/dist-template/interface
--- a/src/Tools/jEdit/dist-template/interface	Tue Oct 21 23:16:03 2008 +0200
+++ b/src/Tools/jEdit/dist-template/interface	Tue Oct 21 23:52:17 2008 +0200
@@ -91,4 +91,5 @@
 export JEDIT_LOGIC JEDIT_PRINT_MODE
 
 exec "$ISABELLE_TOOL" java $JEDIT_JAVA_OPTIONS \
-  -jar "$JEDIT_HOME/jedit.jar" "-settings=$ISABELLE_HOME_USER/jedit" $JEDIT_OPTIONS $FILES
+  -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \
+  "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" $JEDIT_OPTIONS $FILES