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