# HG changeset patch
# User wenzelm
# Date 1308999466 -7200
# Node ID a1ed0456b7e6abdc581dbb9f8e4a028af345fe0a
# Parent  71aba8ee3b8f74364147356dd20478558a10ef3c
clarified java.ext.dirs: putting Isabelle extensions first makes it work miraculously even on Cygwin with Java in "C:\Program Files\..." (with spaces in file name);

diff -r 71aba8ee3b8f -r a1ed0456b7e6 src/Pure/System/Java_Ext_Dirs.java
--- a/src/Pure/System/Java_Ext_Dirs.java	Sat Jun 25 12:54:32 2011 +0200
+++ b/src/Pure/System/Java_Ext_Dirs.java	Sat Jun 25 12:57:46 2011 +0200
@@ -10,12 +10,12 @@
 {
   public static void main(String [] args) {
     StringBuilder s = new StringBuilder();
-    s.append(System.getProperty("java.ext.dirs"));
     int i;
     for (i = 0; i < args.length; i++) {
+      s.append(args[i]);
       s.append(System.getProperty("path.separator"));
-      s.append(args[i]);
     }
+    s.append(System.getProperty("java.ext.dirs"));
     System.out.println(s.toString());
   }
 }