equal
deleted
inserted
replaced
29 try File.rm err_path; |
29 try File.rm err_path; |
30 try File.rm pid_path); |
30 try File.rm pid_path); |
31 val _ = cleanup_files (); |
31 val _ = cleanup_files (); |
32 |
32 |
33 val system_thread = |
33 val system_thread = |
34 Simple_Thread.fork false (fn () => |
34 Simple_Thread.fork {stack_limit = NONE, interrupts = false} (fn () => |
35 Multithreading.with_attributes Multithreading.private_interrupts (fn _ => |
35 Multithreading.with_attributes Multithreading.private_interrupts (fn _ => |
36 let |
36 let |
37 val _ = File.write script_path script; |
37 val _ = File.write script_path script; |
38 val bash_script = |
38 val bash_script = |
39 "exec bash " ^ |
39 "exec bash " ^ |