diff -r ccffb3f9f42b -r 30f6617c9986 src/Pure/System/Java_Ext_Dirs.java
--- a/src/Pure/System/Java_Ext_Dirs.java	Mon Nov 07 14:16:01 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-/*  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();
-    int i;
-    for (i = 0; i < args.length; i++) {
-      s.append(args[i]);
-      s.append(System.getProperty("path.separator"));
-    }
-    s.append(System.getProperty("java.ext.dirs"));
-    System.out.println(s.toString());
-  }
-}
-