[isabelle-dev] Generated files in Codegen

Makarius makarius at sketis.net
Mon Aug 20 17:42:39 CEST 2012


On Mon, 20 Aug 2012, Tobias Nipkow wrote:

> I just rebuilt HOL. As a result I modified 3 files
>
> M doc-src/Codegen/Thy/document/Introduction.tex
> M doc-src/Codegen/Thy/document/Refinement.tex
> M doc-src/Codegen/Thy/examples/example.ML
>
> I suspect these are generated files and that the changes are the result 
> of this changeset: 441a4eed7823
>
> But can I check the changes in?

I've done this already in 881e8a96e617.

As usual I've made some eye-balling to guess if the change of the 
generated files make sense, i.e. is a consequence of something like 
441a4eed7823 above, not a breakdown of the document preparation system.

Anyway, this ancient ritual with the generated files will come to an end 
once that I've resolve the last minor issues with the doc-src build 
configuration.  Afterwards the manuals will just come out of a regular 
session build.


 	Makarius



More information about the isabelle-dev mailing list