| changeset 6028 | 1bfd52528bde |
| parent 6014 | bfd4923b0957 |
| child 6057 | 395ea7617554 |
--- a/NEWS Fri Dec 11 18:56:30 1998 +0100 +++ b/NEWS Fri Dec 11 18:57:00 1998 +0100 @@ -13,6 +13,10 @@ * in locales, the "assumes" and "defines" parts may be omitted if empty; +* new print_mode "xsymbols" for extended symbol support + (e.g. genuiely long arrows) + + *** Internal programming interfaces *** * tuned current_goals_markers semantics: begin / end goal avoids