# HG changeset patch
# User wenzelm
# Date 1621977509 -7200
# Node ID 04d39959d1e64ebc036a218e655f4afe2aa2780f
# Parent  e4d50a660140a7436f457e3e6a2fc506393813f6
tuned signature;

diff -r e4d50a660140 -r 04d39959d1e6 src/Pure/Thy/document_build.scala
--- 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)