# HG changeset patch # User wenzelm # Date 1717247583 -7200 # Node ID a2cf0318db4a56d82eff54582e3e753c899ccaf6 # Parent cb4b21b7b473d7784b51e4fe9fc11adba1c9beeb clarified signature: support explicit cwd; diff -r cb4b21b7b473 -r a2cf0318db4a src/Pure/System/other_isabelle.scala --- a/src/Pure/System/other_isabelle.scala Sat Jun 01 15:11:46 2024 +0200 +++ b/src/Pure/System/other_isabelle.scala Sat Jun 01 15:13:03 2024 +0200 @@ -43,19 +43,20 @@ /* static system */ - def bash_context(script: String): String = + def bash_context(script: String, cwd: Path = isabelle_home): String = Bash.context(script, user_home = ssh.user_home, isabelle_identifier = isabelle_identifier, - cwd = isabelle_home) + cwd = cwd) def bash( script: String, + cwd: Path = isabelle_home, redirect: Boolean = false, echo: Boolean = false, strict: Boolean = true ): Process_Result = { - ssh.execute(bash_context(script), + ssh.execute(bash_context(script, cwd = cwd), progress_stdout = progress.echo_if(echo, _), progress_stderr = progress.echo_if(echo, _), redirect = redirect,