# HG changeset patch # User haftmann # Date 1340774972 -7200 # Node ID 1a6fa9b8140c25026671215d5435302a48ff79f7 # Parent 2709937c74303f252a2ccb5b694e742c7eb14049 corrected name of components file diff -r 2709937c7430 -r 1a6fa9b8140c Admin/mira.py --- a/Admin/mira.py Tue Jun 26 22:52:01 2012 +0200 +++ b/Admin/mira.py Wed Jun 27 07:29:32 2012 +0200 @@ -32,7 +32,7 @@ raise IOError('Bad file: %s' % loc_contrib) subprocess.check_call(['ln', '-s', loc_contrib, '%s/contrib' % loc_isabelle]) - components = path.join(loc_isabelle, 'Admin', 'components.common') + components = path.join(loc_isabelle, 'Admin', 'components') if path.exists(components): components = [] for component in util.readfile_lines(components):