# HG changeset patch # User wenzelm # Date 1432394377 -7200 # Node ID 5ae2a2e74c93eafeb00b1ddeef0404256745ebba # Parent 7c278b692aae516cf376bf8ad52ce2eeb1955fa5 clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature; diff -r 7c278b692aae -r 5ae2a2e74c93 NEWS --- a/NEWS Fri May 22 18:13:31 2015 +0200 +++ b/NEWS Sat May 23 17:19:37 2015 +0200 @@ -133,6 +133,11 @@ antiquotations need to observe the margin explicitly according to Thy_Output.string_of_margin. Minor INCOMPATIBILITY. +* Specification of 'document_files' in the session ROOT file is +mandatory for document preparation. The legacy mode with implicit +copying of the document/ directory is no longer supported. Minor +INCOMPATIBILITY. + *** Pure ***