Fri, 14 Feb 1997 15:16:21 +0100 | wenzelm | semi fix of piping-quit peoblem (should work on systems with *real* sh); | file | diff | annotate |
Thu, 23 Jan 1997 18:16:12 +0100 | wenzelm | 'rm -f' instead of 'mv -f'; | file | diff | annotate |
Wed, 18 Dec 1996 14:31:27 +0100 | wenzelm | fixed EXIT def; | file | diff | annotate |
Mon, 16 Dec 1996 10:29:30 +0100 | wenzelm | SML/NJ startup script (for 0.93). | file | diff | annotate |