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));