NEWS
changeset 3851 fe9932a7cd46
parent 3846 6061fa463784
child 3856 177c64693954
--- a/NEWS	Mon Oct 13 12:48:23 1997 +0200
+++ b/NEWS	Mon Oct 13 12:48:42 1997 +0200
@@ -7,6 +7,8 @@
 
 *** General Changes ***
 
+* print_goals: optional output of const types (set show_consts);
+
 * improved output of warnings (###) / errors (***);
 
 * removed old README and Makefiles;