equal
deleted
inserted
replaced
8 |
8 |
9 |
9 |
10 object Component_Cygwin { |
10 object Component_Cygwin { |
11 val default_mirror: String = "https://isabelle.sketis.net/cygwin_2022" |
11 val default_mirror: String = "https://isabelle.sketis.net/cygwin_2022" |
12 |
12 |
13 val packages: List[String] = List("curl", "libgmp-devel", "nano", "openssh") |
13 val packages: List[String] = List("curl", "libgmp-devel", "nano", "openssh", "perl", "rlwrap") |
14 |
14 |
15 def build_cygwin( |
15 def build_cygwin( |
16 target_dir: Path = Path.current, |
16 target_dir: Path = Path.current, |
17 mirror: String = default_mirror, |
17 mirror: String = default_mirror, |
18 more_packages: List[String] = Nil, |
18 more_packages: List[String] = Nil, |