Fri, 25 Apr 1997 15:06:21 +0200 | wenzelm | no longer forces default; | file | diff | annotate |
Fri, 07 Mar 1997 14:51:50 +0100 | wenzelm | tuned comments; | file | diff | annotate |
Fri, 07 Mar 1997 09:43:31 +0100 | wenzelm | tuned comment; | file | diff | annotate |
Mon, 17 Feb 1997 17:22:50 +0100 | wenzelm | file moved here; | file | diff | annotate |