Mon, 27 Nov 1995 13:37:13 +0100 renamed make_chart to finish_html
clasohm [Mon, 27 Nov 1995 13:37:13 +0100] rev 1368
renamed make_chart to finish_html
Fri, 24 Nov 1995 11:46:23 +0100 fixed make_html bug
clasohm [Fri, 24 Nov 1995 11:46:23 +0100] rev 1367
fixed make_html bug
Fri, 24 Nov 1995 09:27:19 +0100 Inserted warning about defs with extra vars on rhs.
nipkow [Fri, 24 Nov 1995 09:27:19 +0100] rev 1366
Inserted warning about defs with extra vars on rhs.
(0) -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip