proper output of document sources (cf. d892f6d66402);
authorwenzelm
Mon, 23 Nov 2020 13:37:10 +0100
changeset 72690 53064415757a
parent 72685 a7877e14e7f8
child 72691 2126cf946086
proper output of document sources (cf. d892f6d66402);
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 =>