# HG changeset patch
# User wenzelm
# Date 1550247009 -3600
# Node ID 9487788a94c1b4a88767a3ce1adf532531abda1d
# Parent  18f61ce86425873ad2eb44bf23bcc10b325962d1
clarified meta_digest: export_files is a directive for physical output from existing build database;

diff -r 18f61ce86425 -r 9487788a94c1 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Feb 15 17:00:21 2019 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Feb 15 17:10:09 2019 +0100
@@ -573,7 +573,7 @@
 
       val meta_digest =
         SHA1.digest((name, chapter, entry.parent, entry.options, entry.imports,
-          entry.theories_no_position, conditions, entry.document_files, entry.export_files).toString)
+          entry.theories_no_position, conditions, entry.document_files).toString)
 
       Info(name, chapter, dir_selected, entry.pos, entry.groups,
         dir + Path.explode(entry.path), entry.parent, entry.description, session_options,