> Latex tests add very little information for the extra time. It is
> usually easy to figure out what needs to be done to make a broken
> document work again. Moreover, the test often fails because of bad latex
> installations, not because of bad documents.
I disagree. 0% of LaTeX failures observed on the new infrastructure are
spurious, so I'm inclined to keep them running.
Even more so because I will flip the switch to have Jenkins generate
devel.isa-afp.org including browser_info and documents this weekend.
isabelle-dev mailing list