# HG changeset patch
# User wenzelm
# Date 1700332282 -3600
# Node ID ee8c014526dcd866dbd3953e786340a951b609ca
# Parent  3fb4dbffca79175f99add4ab39edf3fdf9dee3ae
avoid duplicate data;

diff -r 3fb4dbffca79 -r ee8c014526dc src/Pure/Admin/build_status.scala
--- 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