# HG changeset patch
# User wenzelm
# Date 1606135030 -3600
# Node ID 53064415757a941f48f6483774839f4a00c405c4
# Parent  a7877e14e7f8d2c7d65bc766b2081464ca790a4c
proper output of document sources (cf. d892f6d66402);

diff -r a7877e14e7f8 -r 53064415757a src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sun Nov 22 13:31:33 2020 +0100
+++ b/src/Pure/Tools/dump.scala	Mon Nov 23 13:37:10 2020 +0100
@@ -59,8 +59,9 @@
         }),
       Aspect("latex", "generated LaTeX source",
         { case args =>
-            for (entry <- args.snapshot.exports if entry.name == "document.tex")
+            for (entry <- args.snapshot.exports if entry.name.startsWith("document/")) {
               args.write(Path.explode(entry.name), entry.uncompressed())
+            }
         }),
       Aspect("theory", "foundational theory content",
         { case args =>