equal
deleted
inserted
replaced
120 which affects Java native libraries in particular. In |
120 which affects Java native libraries in particular. In |
121 Isabelle/Scala the function isabelle.Platform.jvm_platform |
121 Isabelle/Scala the function isabelle.Platform.jvm_platform |
122 identifies the JVM platform. Since a particular Java version is |
122 identifies the JVM platform. Since a particular Java version is |
123 always bundled with Isabelle, the resulting settings also provide |
123 always bundled with Isabelle, the resulting settings also provide |
124 some clues about its platform, without running it. |
124 some clues about its platform, without running it. |
|
125 |
|
126 * Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are |
|
127 notoriously non-portable an should be avoided. |