HomeIsabelle/Phabricator

Implement Unix.executeInEnv and hence Unix.execute largely in C rather

Description

Implement Unix.executeInEnv and hence Unix.execute largely in C rather
than ML. This avoids the possibility that the child process may have to
GC before it can exec.

Details

Provenance
dcjmAuthored on Fri, Apr 16, 5:12 PM
Parents
rPOLYMLa9a1347362b3: Update the Windows library code for the FFI changes.
Branches
Unknown
Tags
Unknown