| Tue, 29 Aug 2000 20:13:17 +0200 | wenzelm | added indent; | changeset | files |
| Tue, 29 Aug 2000 20:12:54 +0200 | wenzelm | \<dots> syntax; | changeset | files |
| Tue, 29 Aug 2000 20:12:35 +0200 | wenzelm | added antiquotation 'name' and option 'indent'; | changeset | files |