Admin/mira.py
changeset 48149 9cb0abdf7c07
parent 47897 9d978604aee4
child 48155 1a6fa9b8140c
equal deleted inserted replaced
48148:84395a03abbb 48149:9cb0abdf7c07
    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     contributed_components = path.join(loc_isabelle, 'Admin', 'contributed_components')
    35     components = path.join(loc_isabelle, 'Admin', 'components.common')
    36     if path.exists(contributed_components):
    36     if path.exists(components):
    37         components = []
    37         components = []
    38         for component in util.readfile_lines(contributed_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):
    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: