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 <ebe...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
