# HG changeset patch
# User oheimb
# Date 913399020 -3600
# Node ID 1bfd52528bdeb77e8d4b8ce338373fe178ed8f83
# Parent  9dd06eeda95ccddc280f4ba82944a73284ae6b58
*** empty log message ***

diff -r 9dd06eeda95c -r 1bfd52528bde NEWS
--- 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