changeset 69650 | c95edf19133b |
parent 69649 | e61b0b819d28 |
child 69660 | 2bc2a8599369 |
--- a/src/Tools/Code/code_target.ML Sun Jan 13 20:25:41 2019 +0100 +++ b/src/Tools/Code/code_target.ML Mon Jan 14 13:58:12 2019 +0100 @@ -177,7 +177,7 @@ ()); fun export_information thy name content = - (Export.export thy name [content]; Export.information thy ""); + (Export.export thy name [content]; writeln (Export.message thy "")); fun export_to_exports thy width (Singleton (extension, p)) = export_information thy (generatedN ^ "." ^ extension) (Code_Printer.format [] width p)