--- a/src/Tools/JVM/Java_Ext_Dirs.java Thu Aug 23 20:49:00 2012 +0200
+++ /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());
- }
-}
-