| Sat, 09 Jan 2016 22:22:17 +0100 | wenzelm | generate HTML version of NEWS, with proper symbol rendering; | changeset | files |
| Sat, 09 Jan 2016 22:00:22 +0100 | wenzelm | tuned -- according to ML version; | changeset | files |
| Sat, 09 Jan 2016 20:56:00 +0100 | wenzelm | suppress somewhat pointless description (NB: this is displayed in 'print_methods'); | changeset | files |