20 |
20 |
21 /* index */ |
21 /* index */ |
22 |
22 |
23 def make_index() |
23 def make_index() |
24 { |
24 { |
25 val header = "Isabelle Development Resources" |
25 val redirect = "https://isabelle-dev.sketis.net/home/menu/view/20" |
26 |
26 |
27 HTML.write_document(root, "index.html", |
27 HTML.write_document(root, "index.html", |
28 List(HTML.title(header)), |
28 List( |
29 List(HTML.chapter(header), |
29 XML.Elem(Markup("meta", |
30 HTML.itemize( |
30 List("http-equiv" -> "Refresh", "content" -> ("0; url=" + redirect))), Nil)), |
31 List( |
31 List(HTML.link(redirect, HTML.text("Isabelle Development Resources")))) |
32 HTML.text("Isabelle nightly ") ::: |
|
33 List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) ::: |
|
34 HTML.text(" (for all platforms)"), |
|
35 |
|
36 HTML.text("Cronjob ") ::: List(HTML.link(CRONJOB_LOG, HTML.text("log file"))), |
|
37 |
|
38 HTML.text("Isabelle ") ::: |
|
39 List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) ::: |
|
40 HTML.text(" information"), |
|
41 |
|
42 HTML.text("Database with recent ") ::: |
|
43 List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) ::: |
|
44 HTML.text(" information (e.g. for ") ::: |
|
45 List(HTML.link("https://sqlitebrowser.org", |
|
46 List(HTML.code(HTML.text("sqlitebrowser"))))) ::: |
|
47 HTML.text(")"))))) |
|
48 } |
32 } |
49 |
33 |
50 |
34 |
51 /* release snapshot */ |
35 /* release snapshot */ |
52 |
36 |