equal
deleted
inserted
replaced
10 object Build_Cygwin |
10 object Build_Cygwin |
11 { |
11 { |
12 val default_mirror: String = "https://isabelle.sketis.net/cygwin_2021-1" |
12 val default_mirror: String = "https://isabelle.sketis.net/cygwin_2021-1" |
13 |
13 |
14 val packages: List[String] = |
14 val packages: List[String] = |
15 List("curl", "libgmp-devel", "nano", "rlwrap", "unzip") |
15 List("curl", "libgmp-devel", "nano", "unzip") |
16 |
16 |
17 def build_cygwin(progress: Progress, |
17 def build_cygwin(progress: Progress, |
18 mirror: String = default_mirror, |
18 mirror: String = default_mirror, |
19 more_packages: List[String] = Nil): Unit = |
19 more_packages: List[String] = Nil): Unit = |
20 { |
20 { |