# HG changeset patch
# User wenzelm
# Date 1398778939 -7200
# Node ID 81dc6fffdf30b4a80291d2448f3271d11a243267
# Parent  13ede133f6eb57faaff2b5ba781f09f413e46d43
require explicit 'document_files';

diff -r 13ede133f6eb -r 81dc6fffdf30 NEWS
--- a/NEWS	Tue Apr 29 15:35:40 2014 +0200
+++ b/NEWS	Tue Apr 29 15:42:19 2014 +0200
@@ -672,7 +672,7 @@
 
 *** System ***
 
-* Session ROOT specifications support explicit 'document_files' for
+* Session ROOT specifications require explicit 'document_files' for
 robust dependencies on LaTeX sources.  Only these explicitly given
 files are copied to the document output directory, before document
 processing is started.
diff -r 13ede133f6eb -r 81dc6fffdf30 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Apr 29 15:35:40 2014 +0200
+++ b/src/Pure/Thy/present.ML	Tue Apr 29 15:42:19 2014 +0200
@@ -362,7 +362,7 @@
 
     val _ =
       if not (null jobs) andalso null doc_files then
-        Output.physical_stderr ("### Document preparation for session " ^ quote name ^
+        Output.physical_stderr ("### Legacy feature! Document preparation for session " ^ quote name ^
           " without 'document_files'\n")
       else ();