
<html><head></head><body>Oh, nothing went wrong: Jenkins sent an email immediately after the push, and the status page also indicated the failure. Automation working as expected.<br>

<br>

Cheers<br>

Lars<br><br><div class="gmail_quote">On 19 October 2016 11:11:21 CEST, Makarius <makarius@sketis.net> wrote:<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">

<pre class="k9mail"><blockquote class="gmail_quote" style="margin: 0pt 0pt 1ex 0.8ex; border-left: 1px solid #729fcf; padding-left: 1ex;"> Am Dienstag, den 18.10.2016, 20:40 +0200 schrieb Florian Haftmann:<br /><blockquote class="gmail_quote" style="margin: 0pt 0pt 1ex 0.8ex; border-left: 1px solid #ad7fa8; padding-left: 1ex;"><blockquote class="gmail_quote" style="margin: 0pt 0pt 1ex 0.8ex; border-left: 1px solid #8ae234; padding-left: 1ex;"> *** No such file:<br /> "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Ess<br /> ential_Supremum.thy"<br /></blockquote></blockquote></blockquote><br />On 19/10/16 00:19, Johannes Hölzl wrote:<br /><blockquote class="gmail_quote" style="margin: 0pt 0pt 1ex 0.8ex; border-left: 1px solid #729fcf; padding-left: 1ex;"> My bad, should be fixed now.<br /></blockquote><br />That is the traditional situation that someone pulling from the<br />repository sees a total existence failure and reports it manually on the<br />mailing

list.<br /><br />So far, the main argument for the massive waste of CPU resources by<br />Jenkins was to make that report automatic.<br /><br />What happened that it did not work here?<br /><br /><br />BTW, isabelle could easily detect the situation of missing files in the<br />repository and emit a warning. I will add that in the next round of<br />refinement (after the release).<br /><br /><br /> Makarius<br /><br /><hr /><br />isabelle-dev mailing list<br />isabelle-dev@in.tum.de<br /><a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a><br /></pre></blockquote></div></body></html>