# HG changeset patch # User wenzelm # Date 1602512351 -7200 # Node ID 7bf67a58f54a3e56e10b921eea6ec8dec5186c25 # Parent 549391271e74c520e9c8e3b967094eaeb6f16708 clarified signature; diff -r 549391271e74 -r 7bf67a58f54a src/Pure/Admin/build_polyml.scala --- a/src/Pure/Admin/build_polyml.scala Mon Oct 12 15:58:37 2020 +0200 +++ b/src/Pure/Admin/build_polyml.scala Mon Oct 12 16:19:11 2020 +0200 @@ -72,9 +72,7 @@ if (!Platform.is_windows) Isabelle_System.settings() else Isabelle_System.settings() + ("MSYS" -> mingw.get_root.expand.implode) - if (platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) { - error("""Missing "chrpath" executable on Linux""") - } + if (platform.is_linux) Isabelle_System.require_command("chrpath") /* bash */ diff -r 549391271e74 -r 7bf67a58f54a src/Pure/Admin/build_spass.scala --- a/src/Pure/Admin/build_spass.scala Mon Oct 12 15:58:37 2020 +0200 +++ b/src/Pure/Admin/build_spass.scala Mon Oct 12 16:19:11 2020 +0200 @@ -22,10 +22,7 @@ { Isabelle_System.with_tmp_dir("build")(tmp_dir => { - /* required commands */ - - List("bison", "flex").foreach(cmd => - if (!Isabelle_System.bash(cmd + " --version").ok) error("Missing command: " + cmd)) + Isabelle_System.require_command("bison", "flex") /* component */ diff -r 549391271e74 -r 7bf67a58f54a src/Pure/Admin/build_verit.scala --- a/src/Pure/Admin/build_verit.scala Mon Oct 12 15:58:37 2020 +0200 +++ b/src/Pure/Admin/build_verit.scala Mon Oct 12 16:19:11 2020 +0200 @@ -22,10 +22,7 @@ { Isabelle_System.with_tmp_dir("build")(tmp_dir => { - /* required commands */ - - List("autoconf", "bison", "flex", "wget").foreach(cmd => - if (!Isabelle_System.bash(cmd + " --version").ok) error("Missing command: " + cmd)) + Isabelle_System.require_command("autoconf", "bison", "flex", "wget") /* component */ diff -r 549391271e74 -r 7bf67a58f54a src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Oct 12 15:58:37 2020 +0200 +++ b/src/Pure/System/isabelle_system.scala Mon Oct 12 16:19:11 2020 +0200 @@ -375,9 +375,16 @@ else error("Expected to find GNU tar executable") } + def require_command(cmds: String*) + { + for (cmd <- cmds) { + if (!bash(Bash.string(cmd) + " --version").ok) error("Missing command: " + quote(cmd)) + } + } + private lazy val curl_check: Unit = - try { bash("curl --version").check } - catch { case ERROR(_) => error("Cannot download files: missing curl") } + try { require_command("curl") } + catch { case ERROR(msg) => error(msg + " --- cannot download files") } def download(url: String, file: Path, progress: Progress = new Progress): Unit = {