NEWS
changeset 14972 51f95648abad
parent 14934 bf9f525d4821
child 15011 35be762f58f9
     1.1 --- a/NEWS	Fri Jun 18 20:10:52 2004 +0200
     1.2 +++ b/NEWS	Sun Jun 20 09:26:29 2004 +0200
     1.3 @@ -75,7 +75,8 @@
     1.4    bypassing the standard channels (writeln etc.), or in token
     1.5    translations to produce properly formatted results; Output.raw is
     1.6    required when capturing already output material that will eventually
     1.7 -  be presented to the user a second time.
     1.8 +  be presented to the user a second time.  For the default print mode,
     1.9 +  both Output.output and Output.raw have no effect.
    1.10  
    1.11  
    1.12  *** HOL ***