# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737454534 -3600
# Node ID 88060e644af71b470658fb9549858e9150a90f4a
# Parent  b1e1019a78e4a5e5972fdc5aa5feadece6844458
clarified: more operations;

diff -r b1e1019a78e4 -r 88060e644af7 src/Pure/Build/build_ci.scala
--- a/src/Pure/Build/build_ci.scala	Tue Jan 21 11:14:00 2025 +0100
+++ b/src/Pure/Build/build_ci.scala	Tue Jan 21 11:15:34 2025 +0100
@@ -71,6 +71,8 @@
 
   object Timed {
     def nightly(start: Time = Time.hms(0, 17, 0)): Timed = Timed(Date.Daily(start))
+    def weekly(day: Date.Day = Date.Day.sun, start: Time = Time.hms(0, 17, 0)): Timed =
+      Timed(Date.Weekly(day, Date.Daily(start)))
   }
 
   case class Timed(cycle: Date.Cycle) extends Trigger {