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