author | wenzelm |
Mon, 11 Nov 2013 21:28:08 +0100 | |
changeset 54392 | f14791d4f08d |
parent 53488 | Admin/MacOS/App3/Info.plist-part2@009d3bcf6907 |
child 57411 | 9444489766a1 |
permissions | -rw-r--r-- |
53488
009d3bcf6907
generate application Info.plist based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
1 |
<string>-Disabelle.home=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}</string> |
009d3bcf6907
generate application Info.plist based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
2 |
</array> |
009d3bcf6907
generate application Info.plist based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
3 |
<key>JVMArguments</key> |
009d3bcf6907
generate application Info.plist based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
4 |
<array> |
009d3bcf6907
generate application Info.plist based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
5 |
</array> |
009d3bcf6907
generate application Info.plist based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
6 |
</dict> |
009d3bcf6907
generate application Info.plist based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);
wenzelm
parents:
diff
changeset
|
7 |
</plist> |