Oh, nothing went wrong: Jenkins sent an email immediately after the push, and the status page also indicated the failure. Automation working as expected.
Cheers Lars On 19 October 2016 11:11:21 CEST, Makarius <makar...@sketis.net> wrote: >> Am Dienstag, den 18.10.2016, 20:40 +0200 schrieb Florian Haftmann: >>>> *** No such file: >>>> "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Ess >>>> ential_Supremum.thy" > >On 19/10/16 00:19, Johannes Hölzl wrote: >> My bad, should be fixed now. > >That is the traditional situation that someone pulling from the >repository sees a total existence failure and reports it manually on >the >mailing list. > >So far, the main argument for the massive waste of CPU resources by >Jenkins was to make that report automatic. > >What happened that it did not work here? > > >BTW, isabelle could easily detect the situation of missing files in the >repository and emit a warning. I will add that in the next round of >refinement (after the release). > > > Makarius > >_______________________________________________ >isabelle-dev mailing list >isabelle-...@in.tum.de >https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
