author | blanchet |
Mon, 09 Jul 2012 23:58:05 +0200 | |
changeset 48220 | 999d6a829c28 |
parent 45385 | 7c1375ba1424 |
permissions | -rw-r--r-- |
/* 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()); } }