Error: no such host

Created by: theoryshaw

• Sourcegraph version: Sourcegraph.com
• Platform information: Windows chrome

Steps to reproduce:

go here: https://sourcegraph.com/search?q=context:global+open+repo:%5Egithub%5C.com/IfcOpenShell/IfcOpenShell%24+file:src/ifcopenshell-python&patternType=standard

Expected behavior:

see appropriate search results

Actual behavior:

example of error: git command [git rev-parse e4016313c49e85389ed6e5f2042fda0e5a72c9c1^0] failed (stderr: ""): Post "http://gitserver-17.gitserver:3178/exec": dial tcp: lookup gitserver-17.gitserver on 10.165.0.10:53: no such host