| Tue, 03 Jul 2018 11:00:37 +0200 | wenzelm | more standard headers; | changeset | files |
| Tue, 03 Jul 2018 10:49:44 +0200 | wenzelm | eliminated hard TABs, assuming tabsize=8; | changeset | files |
| Tue, 03 Jul 2018 00:15:16 +0100 | paulson | more latex problems | changeset | files |