NEWS

--- a/NEWS	Fri Jun 18 20:10:52 2004 +0200
+++ b/NEWS	Sun Jun 20 09:26:29 2004 +0200
@@ -75,7 +75,8 @@
   bypassing the standard channels (writeln etc.), or in token
   translations to produce properly formatted results; Output.raw is
   required when capturing already output material that will eventually
-  be presented to the user a second time.
+  be presented to the user a second time.  For the default print mode,
+  both Output.output and Output.raw have no effect.
 
 
 *** HOL ***