src/Pure/System/Java_Ext_Dirs.java

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/Java_Ext_Dirs.java	Thu Jun 23 13:23:00 2011 +0200
@@ -0,0 +1,22 @@
+/*  Title:      Pure/System/Java_Ext_Dirs.java
+    Author:     Makarius
+
+Augment Java extension directories.
+*/
+
+package isabelle;
+
+public class Java_Ext_Dirs
+{
+  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(System.getProperty("path.separator"));
+      s.append(args[i]);
+    }
+    System.out.println(s.toString());
+  }
+}
+