| Fri, 08 Oct 1999 16:05:06 +0200 | wenzelm | improved; | file | diff | annotate |
| Tue, 05 Oct 1999 18:16:41 +0200 | wenzelm | tuned comments; | file | diff | annotate |
| Wed, 14 Jul 1999 13:32:21 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 14 Jul 1999 13:07:09 +0200 | wenzelm | tuned comments; | file | diff | annotate |