--- a/src/Pure/Admin/build_status.scala Sat Nov 18 19:14:59 2023 +0100
+++ b/src/Pure/Admin/build_status.scala Sat Nov 18 19:31:22 2023 +0100
@@ -14,7 +14,8 @@
val default_image_size = (800, 600)
val default_history = 30
- def default_profiles: List[Profile] = Isabelle_Cronjob.build_status_profiles
+ def default_profiles: List[Profile] =
+ Library.distinct(Isabelle_Cronjob.build_status_profiles)
/* data profiles */
@@ -251,7 +252,7 @@
val store = Build_Log.store(options)
using(store.open_database()) { db =>
- for (profile <- profiles.sortBy(_.description)) {
+ for (profile <- Library.distinct(profiles).sortBy(_.description)) {
progress.echo("input " + quote(profile.description))
val afp = profile.afp