| author | hoelzl |
| Thu, 22 Sep 2011 10:02:16 -0400 | |
| changeset 45041 | 0523a6be8ade |
| parent 43541 | a1ed0456b7e6 |
| permissions | -rw-r--r-- |
| 43518 | 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++) {
|
|
|
43541
a1ed0456b7e6
clarified java.ext.dirs: putting Isabelle extensions first makes it work miraculously even on Cygwin with Java in "C:\Program Files\..." (with spaces in file name);
wenzelm
parents:
43518
diff
changeset
|
15 |
s.append(args[i]); |
| 43518 | 16 |
s.append(System.getProperty("path.separator"));
|
17 |
} |
|
|
43541
a1ed0456b7e6
clarified java.ext.dirs: putting Isabelle extensions first makes it work miraculously even on Cygwin with Java in "C:\Program Files\..." (with spaces in file name);
wenzelm
parents:
43518
diff
changeset
|
18 |
s.append(System.getProperty("java.ext.dirs"));
|
| 43518 | 19 |
System.out.println(s.toString()); |
20 |
} |
|
21 |
} |
|
22 |