equal
deleted
inserted
replaced
20 val main_log = main_dir + Path.explode("log/main.log") // owned by log service |
20 val main_log = main_dir + Path.explode("log/main.log") // owned by log service |
21 |
21 |
22 val isabelle_repos = main_dir + Path.explode("isabelle-build_history") |
22 val isabelle_repos = main_dir + Path.explode("isabelle-build_history") |
23 val afp_repos = main_dir + Path.explode("AFP-build_history") |
23 val afp_repos = main_dir + Path.explode("AFP-build_history") |
24 |
24 |
25 val release_snapshot = main_dir + Path.explode("release_snapshot") |
25 val release_snapshot = Path.explode("~/html-data/release_snapshot") |
26 |
26 |
27 |
27 |
28 |
28 |
29 /** particular tasks **/ |
29 /** particular tasks **/ |
30 |
30 |