tuned;
authorwenzelm
Tue Oct 16 22:59:30 2001 +0200 (2001-10-16)
changeset 118141de4a3321976
parent 11813 5ce7346490af
child 11815 ef7619398680
tuned;
NEWS
     1.1 --- a/NEWS	Tue Oct 16 19:56:31 2001 +0200
     1.2 +++ b/NEWS	Tue Oct 16 22:59:30 2001 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  * support bold style (for single symbols only), input syntax is like
     1.5  this: "\<^bold>\<alpha>" or "\<^bold>A";
     1.6  
     1.7 -* \<bullet> is no output as bold \cdot by default, which looks much
     1.8 +* \<bullet> is now output as bold \cdot by default, which looks much
     1.9  better in printed text;
    1.10  
    1.11  * added default LaTeX bindings for \<tturnstile> and \<TTurnstile>;