*** empty log message ***
authoroheimb
Fri Dec 11 18:57:00 1998 +0100 (1998-12-11)
changeset 60281bfd52528bde
parent 6027 9dd06eeda95c
child 6029 30c957a74803
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Fri Dec 11 18:56:30 1998 +0100
     1.2 +++ b/NEWS	Fri Dec 11 18:57:00 1998 +0100
     1.3 @@ -13,6 +13,10 @@
     1.4  
     1.5  * in locales, the "assumes" and "defines" parts may be omitted if empty;
     1.6  
     1.7 +* new print_mode "xsymbols" for extended symbol support 
     1.8 +  (e.g. genuiely long arrows)
     1.9 +
    1.10 +
    1.11  *** Internal programming interfaces ***
    1.12  
    1.13  * tuned current_goals_markers semantics: begin / end goal avoids