# HG changeset patch # User wenzelm # Date 1602357140 -7200 # Node ID d0937d55eb9051771b21c4eaf9a428d1b362a719 # Parent 10c07d224035d5598e4652073a0b1f99b9620571 clarified errors; diff -r 10c07d224035 -r d0937d55eb90 src/Pure/Admin/build_csdp.scala --- a/src/Pure/Admin/build_csdp.scala Sat Oct 10 21:04:49 2020 +0200 +++ b/src/Pure/Admin/build_csdp.scala Sat Oct 10 21:12:20 2020 +0200 @@ -193,7 +193,7 @@ Options are: -D DIR target directory (default ".") - -M DIR msys/mingw root directory (for Windows) + -M DIR msys/mingw root specification for Windows -U URL download URL (default: """" + default_download_url + """") -v verbose diff -r 10c07d224035 -r d0937d55eb90 src/Pure/System/mingw.scala --- a/src/Pure/System/mingw.scala Sat Oct 10 21:04:49 2020 +0200 +++ b/src/Pure/System/mingw.scala Sat Oct 10 21:12:20 2020 +0200 @@ -38,15 +38,15 @@ def get_root: Path = if (!Platform.is_windows) error("Windows platform required") - else if (root.isEmpty) error("Windows platform needs specification of msys root directory") + else if (root.isEmpty) error("Windows platform requires msys/mingw root specification") else root.get def check { if (Platform.is_windows) { get_root - val result = Isabelle_System.bash(bash_command("uname -s")).check - if (!result.out.startsWith("MSYS")) error("Bad msys installation " + get_root) + try { require(Isabelle_System.bash(bash_command("uname -s")).check.out.startsWith("MSYS")) } + catch { case ERROR(_) => error("Bad msys/mingw installation " + get_root) } } } }