# HG changeset patch # User wenzelm # Date 1520019985 -3600 # Node ID 08dc76bf6400017d5a16abf91750ab865757fccf # Parent 94a8fddc1e7c293224b50d44f94b59351d699e85 proper order; diff -r 94a8fddc1e7c -r 08dc76bf6400 src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Fri Mar 02 20:32:39 2018 +0100 +++ b/src/Pure/Admin/build_status.scala Fri Mar 02 20:46:25 2018 +0100 @@ -116,7 +116,7 @@ "status") val date_format = Date.Format("uuuu-MM-dd HH:mm:ss") val records = - for (entry <- entries) yield { + for (entry <- sorted_entries) yield { CSV.Record(name, entry.chapter, date_format(entry.pull_date),