equal
deleted
inserted
replaced
33 try { Bytes.read(Url(cygwin_exe_name)) } |
33 try { Bytes.read(Url(cygwin_exe_name)) } |
34 catch { case ERROR(_) => error("Failed to download " + quote(cygwin_exe_name)) }) |
34 catch { case ERROR(_) => error("Failed to download " + quote(cygwin_exe_name)) }) |
35 |
35 |
36 File.write(cygwin_isabelle + Path.explode("cygwin_mirror"), mirror) |
36 File.write(cygwin_isabelle + Path.explode("cygwin_mirror"), mirror) |
37 |
37 |
38 File.executable(cygwin_exe) |
38 File.set_executable(cygwin_exe, true) |
39 Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check |
39 Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check |
40 |
40 |
41 val res = |
41 val res = |
42 progress.bash( |
42 progress.bash( |
43 File.bash_path(cygwin_exe) + " --site " + Bash.string(mirror) + " --no-verify" + |
43 File.bash_path(cygwin_exe) + " --site " + Bash.string(mirror) + " --no-verify" + |