equal
deleted
inserted
replaced
150 /* build jdk */ |
150 /* build jdk */ |
151 |
151 |
152 def build_jdk( |
152 def build_jdk( |
153 archives: List[Path], |
153 archives: List[Path], |
154 progress: Progress = new Progress, |
154 progress: Progress = new Progress, |
155 target_dir: Path = Path.current) |
155 target_dir: Path = Path.current): Unit = |
156 { |
156 { |
157 if (Platform.is_windows) error("Cannot build jdk on Windows") |
157 if (Platform.is_windows) error("Cannot build jdk on Windows") |
158 |
158 |
159 Isabelle_System.with_tmp_dir("jdk")(dir => |
159 Isabelle_System.with_tmp_dir("jdk")(dir => |
160 { |
160 { |