NEWS

--- a/NEWS	Wed Jul 14 14:20:47 2010 +0200
+++ b/NEWS	Wed Jul 14 14:53:44 2010 +0200
@@ -17,6 +17,9 @@
 
 *** HOL ***
 
+* code generator: export_code without explicit file declaration prints
+to standard output.  INCOMPATIBILITY.
+
 * Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
 respectively.  INCOMPATIBILITY.