| Mon, 16 Dec 1996 09:59:18 +0100 | wenzelm | added symbolinput filter; | changeset | files |
| Mon, 16 Dec 1996 09:58:16 +0100 | wenzelm | symbolinput - translate symbols into \<...> sequences; | changeset | files |
| Mon, 16 Dec 1996 09:57:34 +0100 | wenzelm | renamed to symbolinput.pl; | changeset | files |