--- a/NEWS Wed Jan 16 17:55:26 2019 +0100
+++ b/NEWS Wed Jan 16 17:56:29 2019 +0100
@@ -76,9 +76,10 @@
* Code generation: command 'export_code' without file keyword exports
code as regular theory export, which can be materialized using the
-command-line tool "isabelle export", or browsed in Isabelle/jEdit via
-the "isabelle-export:" file-system. To get generated code dumped into
-output, use "file \<open>\<close>". Minor INCOMPATIBILITY.
+command-line tool "isabelle export" or 'export_files' in the session
+ROOT, or browsed in Isabelle/jEdit via the "isabelle-export:"
+file-system. To get generated code dumped into output, use "file \<open>\<close>".
+Minor INCOMPATIBILITY.
* Simplified syntax setup for big operators under image. In rare
situations, type conversions are not inserted implicitly any longer