> 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. Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
