[isabelle-dev] Jenkins maintenance

[Lawrence Paulson]

I’d be happy with this, if it’s achievable.

I’ve only tried the testboard once or twice; I find it too easy to do the wrong thing when you have a choice of targets to push to, and I have a powerful machine so I prefer to test there. But a mechanism of the sort you describe (provided it’s easy to use) would be ideal.
Larry

> On 3 Oct 2016, at 16:12, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> I for one think that a big improvement would be a system where no one
> pushes to the repository directly: every push goes to a testing server,
> and if the test is successful, the changes can then automatically be
> merged into the repository without an additional test. This avoids the
> current duplication of tests where one first pushes to the testboard,
> waits for everything to run through, and then pushes to the repository
> where everything is tested again.