Mon, 24 Mar 1997 10:28:23 +0100 | paulson | Deleted needless parentheses | changeset | files |
Mon, 24 Mar 1997 10:27:28 +0100 | paulson | Deleted unnecessary rules | changeset | files |
Thu, 20 Mar 1997 19:12:20 +0100 | wenzelm | fixed font names; | changeset | files |