# HG changeset patch # User krauss # Date 1301668198 -7200 # Node ID 5f311600ba2674ddd0ba08f957071317dd4ac9df # Parent 9893b2913a44083e0fbd122107197697df777ff7 fixed accidental redefinition diff -r 9893b2913a44 -r 5f311600ba26 Admin/mira.py --- a/Admin/mira.py Fri Apr 01 15:49:19 2011 +0200 +++ b/Admin/mira.py Fri Apr 01 16:29:58 2011 +0200 @@ -338,7 +338,7 @@ JD_confs = 'JD_NS JD_FTA JD_Hoare JD_SN JD_Arrow JD_FFT JD_Jinja JD_QE JD_S2S'.split(' ') @scheduler() -def judgement_day(env): +def judgement_day_scheduler(env): """Scheduler for Judgement Day.""" return schedule.age_scheduler(env, 'Isabelle', JD_confs)