# HG changeset patch
# User wenzelm
# Date 1547657789 -3600
# Node ID f97fbb2330aa297d7983baeaddd8ba5a72abdaac
# Parent  2486792eaf6121081ebb492c27f82b013ce3b34e
tuned;

diff -r 2486792eaf61 -r f97fbb2330aa NEWS
--- 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