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