# 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)