equal
deleted
inserted
replaced
46 build_library: Boolean = false, |
46 build_library: Boolean = false, |
47 parallel_jobs: Int = 1, |
47 parallel_jobs: Int = 1, |
48 remote_mac: String = ""): Release_Info = |
48 remote_mac: String = ""): Release_Info = |
49 { |
49 { |
50 /* release info */ |
50 /* release info */ |
|
51 |
|
52 Isabelle_System.mkdirs(base_dir) |
51 |
53 |
52 val release_info = |
54 val release_info = |
53 { |
55 { |
54 val date = Date.now() |
56 val date = Date.now() |
55 val name = if (release_name != "") release_name else "Isabelle_" + Date.Format.date(date) |
57 val name = if (release_name != "") release_name else "Isabelle_" + Date.Format.date(date) |