Skip to content
Failed

Changes

Summary

  1. merged
  2. merged
  3. removed obsolete chmod: isabelle_process no longer supports writable heaps;
  4. redundant -- already provided by Poly/ML toplevel;
  5. prefer bash_process;
  6. only one nested bash process (NB: OS.System = vfork + exec /bin/sh in RTS is faster than Posix.Process.fork/exec in ML);
Changeset 62488:bd7358b3ab5e by wenzelm:
merged
Changeset 62487:fc353b09325d by wenzelm:
merged
Changeset 62486:b737f8f37454 by wenzelm:
removed obsolete chmod: isabelle_process no longer supports writable heaps;
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 62485:a04e26352106 by wenzelm:
redundant -- already provided by Poly/ML toplevel;
The file was modified lib/scripts/run-polyml (diff)
Changeset 62484:4759dbb35148 by wenzelm:
prefer bash_process;
The file was modified src/Pure/Concurrent/bash_windows.ML (diff)
Changeset 62483:c13dac251a81 by wenzelm:
only one nested bash process (NB: OS.System = vfork + exec /bin/sh in RTS is faster than Posix.Process.fork/exec in ML);
The file was modified src/Pure/Concurrent/bash.ML (diff)