require explicit 'document_files';
authorwenzelm
Tue Apr 29 15:42:19 2014 +0200 (2014-04-29)
changeset 5678781dc6fffdf30
parent 56786 13ede133f6eb
child 56788 28ff163eefef
require explicit 'document_files';
NEWS
src/Pure/Thy/present.ML
     1.1 --- a/NEWS	Tue Apr 29 15:35:40 2014 +0200
     1.2 +++ b/NEWS	Tue Apr 29 15:42:19 2014 +0200
     1.3 @@ -672,7 +672,7 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 -* Session ROOT specifications support explicit 'document_files' for
     1.8 +* Session ROOT specifications require explicit 'document_files' for
     1.9  robust dependencies on LaTeX sources.  Only these explicitly given
    1.10  files are copied to the document output directory, before document
    1.11  processing is started.
     2.1 --- a/src/Pure/Thy/present.ML	Tue Apr 29 15:35:40 2014 +0200
     2.2 +++ b/src/Pure/Thy/present.ML	Tue Apr 29 15:42:19 2014 +0200
     2.3 @@ -362,7 +362,7 @@
     2.4  
     2.5      val _ =
     2.6        if not (null jobs) andalso null doc_files then
     2.7 -        Output.physical_stderr ("### Document preparation for session " ^ quote name ^
     2.8 +        Output.physical_stderr ("### Legacy feature! Document preparation for session " ^ quote name ^
     2.9            " without 'document_files'\n")
    2.10        else ();
    2.11