--- a/src/Pure/Tools/generated_files.ML Sat Nov 02 10:56:53 2019 +0100
+++ b/src/Pure/Tools/generated_files.ML Sat Nov 02 12:02:27 2019 +0100
@@ -136,7 +136,7 @@
in () end;
fun export_file thy (file: file) =
- Export.export thy (file_binding file) [#content file];
+ Export.export thy (file_binding file) [XML.Text (#content file)];
(* file types *)
@@ -290,7 +290,7 @@
Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding;
in
(if is_some executable then Export.export_executable else Export.export)
- thy binding' [content]
+ thy binding' [XML.Text content]
end));
val _ =
if null export then ()