> Am Dienstag, den 18.10.2016, 20:40 +0200 schrieb Florian Haftmann:
>>> *** No such file:
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
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).
isabelle-dev mailing list