[isabelle-dev] Distro broken

[Lars Hupel]

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 <makarius at 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-dev at in.tum.de
>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161019/f0bc1a3d/attachment-0002.html>