src/Pure/Build/build_ci.scala
changeset 81882 2adff49492f0
parent 80483 5b539d1d3577
child 81884 058f239b860a
equal deleted inserted replaced
81881:f23fc3d21873 81882:2adff49492f0
    77         (before.time < start0.time && start0.time <= now.time) ||
    77         (before.time < start0.time && start0.time <= now.time) ||
    78           (before.time < start1.time && start1.time <= now.time)
    78           (before.time < start1.time && start1.time <= now.time)
    79       }
    79       }
    80   }
    80   }
    81 
    81 
    82   case class Timed(in_interval: (Date, Date) => Boolean) extends Trigger
    82   case class Timed(in_interval: (Date, Date) => Boolean) extends Trigger {
       
    83     def next(before: Date, now: Date): Boolean = in_interval(before, now)
       
    84   }
    83 
    85 
    84 
    86 
    85   /* build hooks */
    87   /* build hooks */
    86 
    88 
    87   trait Hook {
    89   trait Hook {