Hans-Christoph Steiner 58b38a42d4 rename default_repo.xml to default_repos.xml, there are many
Just to make it clear that there can be and are multiple repos configured
in the file.
2016-10-25 11:54:40 +03:30
..
2016-10-25 11:54:40 +03:30