src/Pure/Admin/build_status.scala
changeset 67749 08dc76bf6400
parent 67739 e512938b853c
child 67759 56eba30e7b99
equal deleted inserted replaced
67748:94a8fddc1e7c 67749:08dc76bf6400
   114           "average_heap",
   114           "average_heap",
   115           "stored_heap",
   115           "stored_heap",
   116           "status")
   116           "status")
   117       val date_format = Date.Format("uuuu-MM-dd HH:mm:ss")
   117       val date_format = Date.Format("uuuu-MM-dd HH:mm:ss")
   118       val records =
   118       val records =
   119         for (entry <- entries) yield {
   119         for (entry <- sorted_entries) yield {
   120           CSV.Record(name,
   120           CSV.Record(name,
   121             entry.chapter,
   121             entry.chapter,
   122             date_format(entry.pull_date),
   122             date_format(entry.pull_date),
   123             entry.afp_pull_date match { case Some(date) => date_format(date) case None => "" },
   123             entry.afp_pull_date match { case Some(date) => date_format(date) case None => "" },
   124             entry.isabelle_version,
   124             entry.isabelle_version,