--- a/src/Pure/Thy/document_build.scala Tue May 25 23:12:46 2021 +0200
+++ b/src/Pure/Thy/document_build.scala Tue May 25 23:18:29 2021 +0200
@@ -426,7 +426,7 @@
/* build documents */
def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
- def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name)
+ def document_tex_name(name: Document.Node.Name): String = Export.DOCUMENT_PREFIX + tex_name(name)
class Build_Error(val log_lines: List[String], val message: String)
extends Exn.User_Error(message)