AW: gcc git repository issue?

["Warlich, Christof" <christof dot warlich at siemens dot com>]

> If you use git:// you won't see this problem.

Thanks :-), that fixed the problem indeed.

> I don't know what causes it though.  Maybe some misconfigured caching
> server, either somewhere in your network or on gcc.gnu.org?

Just in case that someone who volunteers to maintain gcc.gnu.org finds this
information useful: The issue (when using the https protocol) does not only
show up in our (proxied) company network, but also at home, i.e. without any
proxy inbetween. This, together with the fact that we only saw the issue with
the gcc.gnu.org repository so far, seems to be an indicator that the
misconfiguration is within the network of gcc.gnu.org.

But anyhow, I'm fine using the git protocol ...