Fix bug 1747 to allow installation without docker proxy
[osm/devops.git] / tools / .gitignore
1 repos/*