Mon, 17 Apr 2000 14:27:10 +0200 made SML/NJ happy;
wenzelm [Mon, 17 Apr 2000 14:27:10 +0200] rev 8731
made SML/NJ happy;
Mon, 17 Apr 2000 14:20:41 +0200 made SML/NJ happy;
wenzelm [Mon, 17 Apr 2000 14:20:41 +0200] rev 8730
made SML/NJ happy;
Mon, 17 Apr 2000 14:12:33 +0200 * improved name spaces: ambiguous output is qualified; support for
wenzelm [Mon, 17 Apr 2000 14:12:33 +0200] rev 8729
* improved name spaces: ambiguous output is qualified; support for hiding of names;
Mon, 17 Apr 2000 14:10:38 +0200 improved output of ambiguous entries;
wenzelm [Mon, 17 Apr 2000 14:10:38 +0200] rev 8728
improved output of ambiguous entries; support hiding;
Mon, 17 Apr 2000 14:10:04 +0200 Pretty.chunks;
wenzelm [Mon, 17 Apr 2000 14:10:04 +0200] rev 8727
Pretty.chunks;
Mon, 17 Apr 2000 14:08:51 +0200 'global' / 'local': comment;
wenzelm [Mon, 17 Apr 2000 14:08:51 +0200] rev 8726
'global' / 'local': comment; added 'hide';
Mon, 17 Apr 2000 14:08:19 +0200 name space hide operations;
wenzelm [Mon, 17 Apr 2000 14:08:19 +0200] rev 8725
name space hide operations;
Mon, 17 Apr 2000 14:07:00 +0200 global/local_path: comment;
wenzelm [Mon, 17 Apr 2000 14:07:00 +0200] rev 8724
global/local_path: comment; added name space hide;
Mon, 17 Apr 2000 14:06:05 +0200 added 'hide';
wenzelm [Mon, 17 Apr 2000 14:06:05 +0200] rev 8723
added 'hide';
Mon, 17 Apr 2000 14:04:46 +0200 tuned msg;
wenzelm [Mon, 17 Apr 2000 14:04:46 +0200] rev 8722
tuned msg;
(0) -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip