src/Pure/Thy/thy_info.ML
changeset 69784 24bbc4e30e5b
parent 68839 d8251a61cce8
child 69877 45b2e784350a
--- a/src/Pure/Thy/thy_info.ML	Sat Feb 02 14:51:11 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Feb 02 15:52:14 2019 +0100
@@ -66,7 +66,7 @@
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
             val _ =
               if Options.bool options "export_document"
-              then Export.export thy "document.tex" output else ();
+              then Export.export thy (Path.explode "document.tex") output else ();
             val _ = if #enabled option then Present.theory_output thy output else ();
           in () end
       end));