On 24/09/16 16:55, Lars Hupel wrote:
>
> Note that worker allocation is "first come first serve". We currently
> have bandwidth for two AFP and two distribution builds at the same time,
> each taking approx. 80-90 minutes; everything else gets queued. Please
> push responsibly.
This reminds me of a still open question: Why is there this "continuous
integration" on every push anyway?
Somehow the repository events are re-interpreted for batch job
management, but this does not sound like efficient use of CPU resources.
The main purpose of pushing is to publish local changes and thus to
resynchronize with the world out there.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
