[isabelle-dev] Regression test for documents?

[Makarius]

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.


Incidently doc-src is failing again (e.g. in 0162a0d284ac):

*** Failed to finish proof
*** At command "done" (line 378 of "~~/doc-src/TutorialI/CTL/CTL.thy")

This might be related to some recent complete_lattice changes that I've 
seen passing by.


 	Makarius