[isabelle-dev] AODV

[Makarius]

On Wed, 10 Dec 2014, Gerwin Klein wrote:

> “build -a” is still going to miss document preparation errors in the 
> AFP, though, so it’s still not really the right command to run for 
> testing it.

We've had that discussion occasionally.  Nowadays I usually do full "build 
-a -d '$AFP'" quite aggresively, but rarely -o document=pdf.  It is just a 
matter to get the most relevant information out of the test.  Document 
preparation adds very little, and quite often it is just a problem of the 
LaTeX installation anyway.

This canonical "build -a" will eventually become a certain mode of using 
PIDE, but without any add-on features such as -g AFP.


 	Makarius

----------------------------------------------------------------------------
                 https://stop-ttip.org/signatures-member-states
----------------------------------------------------------------------------