*** empty log message ***

--- 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