[isabelle-dev] Regression test for documents?

[Gerwin Klein]

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.

Gerwin