[isabelle-dev] document_output vs. old document_dump/document_dump_mode
makarius at sketis.net
Tue Aug 28 20:06:38 CEST 2012
Are there remaining uses (or users) of the old document_dump /
document_dump_mode options? This corresponds to former options -D and -C
of isabelle usedir.
The meaning of these features has become quite difficult to define, so it
looks like they are better discontinued.
If there are remaining cases of difficult IsaMakefile/usedir
configurations that still use them, they can be discussed here to see if
anything is still missing in the new build tool to replace them.
More information about the isabelle-dev