equal
deleted
inserted
replaced
1 /* Title: Pure/System/Java_Ext_Dirs.java |
|
2 Author: Makarius |
|
3 |
|
4 Augment Java extension directories. |
|
5 */ |
|
6 |
|
7 package isabelle; |
|
8 |
|
9 public class Java_Ext_Dirs |
|
10 { |
|
11 public static void main(String [] args) { |
|
12 StringBuilder s = new StringBuilder(); |
|
13 int i; |
|
14 for (i = 0; i < args.length; i++) { |
|
15 s.append(args[i]); |
|
16 s.append(System.getProperty("path.separator")); |
|
17 } |
|
18 s.append(System.getProperty("java.ext.dirs")); |
|
19 System.out.println(s.toString()); |
|
20 } |
|
21 } |
|
22 |
|