Admin/mira.py
changeset 48181 ea1a8a93ba49
parent 48155 1a6fa9b8140c
child 48182 221a17a97fab
equal deleted inserted replaced
48180:54fd394248aa 48181:ea1a8a93ba49
    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')
    35     components_registry = path.join(loc_isabelle, 'Admin', 'components')
    36     if path.exists(components):
    36     if path.exists(components_registry):
    37         components = []
    37         components = []
    38         for component in util.readfile_lines(components):
    38         for component in util.readfile_lines(components_registry):
    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):
    41                 components.append(loc_component)
    41                 components.append(loc_component)
    42         writer = open(path.join(loc_isabelle, 'etc', 'components'), 'a')
    42         writer = open(path.join(loc_isabelle, 'etc', 'components'), 'a')
    43         for component in components:
    43         for component in components: