[isabelle-dev] Regression test for documents?

Gerwin Klein gerwin.klein at nicta.com.au
Tue Feb 28 21:42:24 CET 2012

On 29/02/2012, at 2:53 AM, Makarius wrote:

> On Sat, 18 Feb 2012, Florian Haftmann wrote:
>> …seems not really operative.  Otherwise accidents like
>> http://isabelle.in.tum.de/reports/Isabelle/rev/2a0e1bcf713c could not
>> have escaped attention for so long.
>> Maybe we could setup a mira test for this, also including the makedist
>> procedure?
> isatest used to do that, but the main crontab on macbroy28 has the following commented out:
> #17 10 * * *                  $HOME/bin/isatest-doc
> Gerwin might know the reason.

I don't. It's possible that it was switched off in the time of random failures two years ago or so.

I'm happy to switch it back on if people care about it.


More information about the isabelle-dev mailing list