Admin/mira.py
changeset 48155 1a6fa9b8140c
parent 48149 9cb0abdf7c07
child 48181 ea1a8a93ba49
equal deleted inserted replaced
48154:2709937c7430 48155:1a6fa9b8140c
    30     loc_contrib = path.expanduser(loc_contrib)
    30     loc_contrib = path.expanduser(loc_contrib)
    31     if not path.exists(loc_contrib):
    31     if not path.exists(loc_contrib):
    32         raise IOError('Bad file: %s' % loc_contrib)
    32         raise IOError('Bad file: %s' % loc_contrib)
    33     subprocess.check_call(['ln', '-s', loc_contrib, '%s/contrib' % loc_isabelle])
    33     subprocess.check_call(['ln', '-s', loc_contrib, '%s/contrib' % loc_isabelle])
    34 
    34 
    35     components = path.join(loc_isabelle, 'Admin', 'components.common')
    35     components = path.join(loc_isabelle, 'Admin', 'components')
    36     if path.exists(components):
    36     if path.exists(components):
    37         components = []
    37         components = []
    38         for component in util.readfile_lines(components):
    38         for component in util.readfile_lines(components):
    39             loc_component = path.join(loc_isabelle, component)
    39             loc_component = path.join(loc_isabelle, component)
    40             if path.exists(loc_component):
    40             if path.exists(loc_component):