27 |
27 |
28 def bash(script: String, |
28 def bash(script: String, |
29 cwd: JFile = null, |
29 cwd: JFile = null, |
30 env: Map[String, String] = Isabelle_System.settings(), |
30 env: Map[String, String] = Isabelle_System.settings(), |
31 redirect: Boolean = false, |
31 redirect: Boolean = false, |
32 echo: Boolean = false): Process_Result = |
32 echo: Boolean = false, |
|
33 strict: Boolean = true): Process_Result = |
33 { |
34 { |
34 Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, |
35 Isabelle_System.bash(script, cwd = cwd, env = env, redirect = redirect, |
35 progress_stdout = echo_if(echo, _), |
36 progress_stdout = echo_if(echo, _), |
36 progress_stderr = echo_if(echo, _)) |
37 progress_stderr = echo_if(echo, _), |
|
38 strict = strict) |
37 } |
39 } |
38 } |
40 } |
39 |
41 |
40 object No_Progress extends Progress |
42 object No_Progress extends Progress |
41 |
43 |