equal
deleted
inserted
replaced
38 val bash_script = |
38 val bash_script = |
39 "exec bash " ^ |
39 "exec bash " ^ |
40 File.shell_path script_path ^ |
40 File.shell_path script_path ^ |
41 " > " ^ File.shell_path out_path ^ |
41 " > " ^ File.shell_path out_path ^ |
42 " 2> " ^ File.shell_path err_path; |
42 " 2> " ^ File.shell_path err_path; |
|
43 val _ = getenv_strict "EXEC_PROCESS"; |
43 val status = |
44 val status = |
44 OS.Process.system |
45 OS.Process.system |
45 (if getenv "EXEC_PROCESS" = "" then |
46 ("exec \"$EXEC_PROCESS\" " ^ File.shell_path pid_path ^ " " ^ quote bash_script); |
46 ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ |
|
47 File.shell_path pid_path ^ " script " ^ quote bash_script) |
|
48 else |
|
49 ("exec \"$EXEC_PROCESS\" " ^ |
|
50 File.shell_path pid_path ^ " " ^ quote bash_script)); |
|
51 val res = |
47 val res = |
52 (case Posix.Process.fromStatus status of |
48 (case Posix.Process.fromStatus status of |
53 Posix.Process.W_EXITED => Result 0 |
49 Posix.Process.W_EXITED => Result 0 |
54 | Posix.Process.W_EXITSTATUS 0wx82 => Signal |
50 | Posix.Process.W_EXITSTATUS 0wx82 => Signal |
55 | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) |
51 | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) |