equal
deleted
inserted
replaced
36 let |
36 let |
37 val _ = File.write script_path script; |
37 val _ = File.write script_path script; |
38 val _ = getenv_strict "ISABELLE_BASH_PROCESS"; |
38 val _ = getenv_strict "ISABELLE_BASH_PROCESS"; |
39 val status = |
39 val status = |
40 OS.Process.system |
40 OS.Process.system |
41 ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.shell_path pid_path ^ |
41 ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ |
42 " bash " ^ File.shell_path script_path ^ |
42 " bash " ^ File.bash_path script_path ^ |
43 " > " ^ File.shell_path out_path ^ |
43 " > " ^ File.bash_path out_path ^ |
44 " 2> " ^ File.shell_path err_path); |
44 " 2> " ^ File.bash_path err_path); |
45 val res = |
45 val res = |
46 (case Posix.Process.fromStatus status of |
46 (case Posix.Process.fromStatus status of |
47 Posix.Process.W_EXITED => Result 0 |
47 Posix.Process.W_EXITED => Result 0 |
48 | Posix.Process.W_EXITSTATUS 0wx82 => Signal |
48 | Posix.Process.W_EXITSTATUS 0wx82 => Signal |
49 | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) |
49 | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) |