Roman Hodek <Roman.Hodek@informatik.uni-erlangen.de> writes: > Today's problem seems to be only a problem for today... Also the push > mirrors have the bad data, so it seems master started the push too > early. The same script which runs the archive triggers the pushes, so that can't happen. Guy