clarified website: redirect to isabelle-dev Phabricator Overview;
authorwenzelm
Wed, 11 Dec 2019 19:14:49 +0100
changeset 71272 1e7319957408
parent 71271 58aa62b8c6d3
child 71273 6b8cbdc9713b
clarified website: redirect to isabelle-dev Phabricator Overview;
src/Pure/Admin/isabelle_devel.scala
--- a/src/Pure/Admin/isabelle_devel.scala	Wed Dec 11 16:47:33 2019 +0100
+++ b/src/Pure/Admin/isabelle_devel.scala	Wed Dec 11 19:14:49 2019 +0100
@@ -22,29 +22,13 @@
 
   def make_index()
   {
-    val header = "Isabelle Development Resources"
+    val redirect = "https://isabelle-dev.sketis.net/home/menu/view/20"
 
     HTML.write_document(root, "index.html",
-      List(HTML.title(header)),
-      List(HTML.chapter(header),
-        HTML.itemize(
-          List(
-            HTML.text("Isabelle nightly ") :::
-            List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) :::
-            HTML.text(" (for all platforms)"),
-
-            HTML.text("Cronjob ") ::: List(HTML.link(CRONJOB_LOG, HTML.text("log file"))),
-
-            HTML.text("Isabelle ") :::
-            List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) :::
-            HTML.text(" information"),
-
-            HTML.text("Database with recent ") :::
-            List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
-            HTML.text(" information (e.g. for ") :::
-            List(HTML.link("https://sqlitebrowser.org",
-              List(HTML.code(HTML.text("sqlitebrowser"))))) :::
-            HTML.text(")")))))
+      List(
+        XML.Elem(Markup("meta",
+          List("http-equiv" -> "Refresh", "content" -> ("0; url=" + redirect))), Nil)),
+      List(HTML.link(redirect, HTML.text("Isabelle Development Resources"))))
   }