equal
deleted
inserted
replaced
72 error("Windows requires specification of msys root directory") |
72 error("Windows requires specification of msys root directory") |
73 case None => Isabelle_System.settings() |
73 case None => Isabelle_System.settings() |
74 case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode) |
74 case Some(msys) => Isabelle_System.settings() + ("MSYS" -> msys.expand.implode) |
75 } |
75 } |
76 |
76 |
|
77 if (Platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) { |
|
78 error("""Missing "chrpath" executable on Linux""") |
|
79 } |
|
80 |
77 |
81 |
78 /* bash */ |
82 /* bash */ |
79 |
83 |
80 def bash( |
84 def bash( |
81 cwd: Path, script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = |
85 cwd: Path, script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = |