equal
deleted
inserted
replaced
970 exhaust the small 32-bit address space of the ML process (which is used |
970 exhaust the small 32-bit address space of the ML process (which is used |
971 by default). |
971 by default). |
972 |
972 |
973 * System option "ML_process_policy" specifies an optional command prefix |
973 * System option "ML_process_policy" specifies an optional command prefix |
974 for the underlying ML process, e.g. to control CPU affinity on |
974 for the underlying ML process, e.g. to control CPU affinity on |
975 multiprocessor systems. |
975 multiprocessor systems. The "isabelle jedit" tool allows to override the |
976 |
976 implicit default via option -p. |
977 * The "isabelle jedit" tool provides options -P and -p to specify an |
|
978 optional command prefix for the Java and ML process, respectively (see |
|
979 also option "ML_process_policy"). |
|
980 |
977 |
981 |
978 |
982 |
979 |
983 New in Isabelle2016 (February 2016) |
980 New in Isabelle2016 (February 2016) |
984 ----------------------------------- |
981 ----------------------------------- |