equal
deleted
inserted
replaced
23 val _ = write_file script_name script; |
23 val _ = write_file script_name script; |
24 |
24 |
25 val output_name = OS.FileSys.tmpName (); |
25 val output_name = OS.FileSys.tmpName (); |
26 |
26 |
27 val status = |
27 val status = |
28 OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" nogroup /dev/null" ^ |
28 OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^ |
29 " \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\""); |
29 " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\""); |
30 val rc = |
30 val rc = |
31 (case Posix.Process.fromStatus status of |
31 (case Posix.Process.fromStatus status of |
32 Posix.Process.W_EXITED => 0 |
32 Posix.Process.W_EXITED => 0 |
33 | Posix.Process.W_EXITSTATUS w => Word8.toInt w |
33 | Posix.Process.W_EXITSTATUS w => Word8.toInt w |
34 | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s) |
34 | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s) |