clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature; Isabelle2015
authorwenzelm
Sat May 23 17:19:37 2015 +0200 (2015-05-23)
changeset 602995ae2a2e74c93
parent 60298 7c278b692aae
child 60300 82453d0f49ee
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
NEWS
     1.1 --- a/NEWS	Fri May 22 18:13:31 2015 +0200
     1.2 +++ b/NEWS	Sat May 23 17:19:37 2015 +0200
     1.3 @@ -133,6 +133,11 @@
     1.4  antiquotations need to observe the margin explicitly according to
     1.5  Thy_Output.string_of_margin. Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Specification of 'document_files' in the session ROOT file is
     1.8 +mandatory for document preparation. The legacy mode with implicit
     1.9 +copying of the document/ directory is no longer supported. Minor
    1.10 +INCOMPATIBILITY.
    1.11 +
    1.12  
    1.13  *** Pure ***
    1.14