changeset 72690 | 53064415757a |
parent 72375 | e48d93811ed7 |
child 72691 | 2126cf946086 |
--- 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 =>