# HG changeset patch
# User wenzelm
# Date 1700337104 -3600
# Node ID d8352eb7aa7b3bb0d1c9db1b6c5b1c6b56186579
# Parent  ee8c014526dcd866dbd3953e786340a951b609ca
tuned;

diff -r ee8c014526dc -r d8352eb7aa7b src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 18 19:31:22 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 18 20:51:44 2023 +0100
@@ -127,8 +127,8 @@
     def versions: (String, Option[String]) = (isabelle_version, afp_version)
 
     def known_versions(rev: String, afp_rev: Option[String]): Boolean =
-      known && rev != "" && isabelle_version == rev &&
-      (afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev)
+      known && rev.nonEmpty && isabelle_version == rev &&
+      (afp_rev.isEmpty || afp_rev.get.nonEmpty && afp_version == afp_rev)
   }
 
   def recent_items(
@@ -490,7 +490,7 @@
     val hostname: String = Isabelle_System.hostname()
 
     def log(date: Date, task_name: String, msg: String): Unit =
-      if (task_name != "") {
+      if (task_name.nonEmpty) {
         thread.send(
           "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
       }
@@ -579,7 +579,7 @@
         for {
           t <- tasks.iterator
           task <- t()
-          if !exclude_task(task.name) || task.name == ""
+          if !exclude_task(task.name) || task.name.isEmpty
         } run_now(task))
 
     def SEQUENTIAL(tasks: Logger_Task*): Logger_Task =