equal
deleted
inserted
replaced
52 |
52 |
53 def release_snapshot( |
53 def release_snapshot( |
54 options: Options, |
54 options: Options, |
55 rev: String = "", |
55 rev: String = "", |
56 afp_rev: String = "", |
56 afp_rev: String = "", |
57 parallel_jobs: Int = 1, |
57 parallel_jobs: Int = 1) |
58 remote_mac: String = "") |
|
59 { |
58 { |
60 Isabelle_System.with_tmp_dir("isadist")(base_dir => |
59 Isabelle_System.with_tmp_dir("isadist")(base_dir => |
61 { |
60 { |
62 Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT), |
61 Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT), |
63 website_dir => |
62 website_dir => |
64 Build_Release.build_release(base_dir, options, rev = rev, afp_rev = afp_rev, |
63 Build_Release.build_release(base_dir, options, rev = rev, afp_rev = afp_rev, |
65 parallel_jobs = parallel_jobs, remote_mac = remote_mac, website = Some(website_dir))) |
64 parallel_jobs = parallel_jobs, website = Some(website_dir))) |
66 }) |
65 }) |
67 } |
66 } |
68 |
67 |
69 |
68 |
70 /* maintain build_log database */ |
69 /* maintain build_log database */ |