| Sat, 24 Jun 2017 11:02:32 +0200 | wenzelm | clarified indentation; | changeset | files |
| Fri, 23 Jun 2017 22:25:50 +0200 | wenzelm | merged | changeset | files |
| Fri, 23 Jun 2017 22:21:11 +0200 | wenzelm | tuned signature; | changeset | files |
| Fri, 23 Jun 2017 22:07:12 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 23 Jun 2017 22:04:14 +0200 | wenzelm | NEWS; | changeset | files |
| Fri, 23 Jun 2017 22:03:51 +0200 | wenzelm | indentation of keywords after input; | changeset | files |
| Fri, 23 Jun 2017 16:16:41 +0200 | wenzelm | indent = 0 for blank lines: produce less whitespace by default; | changeset | files |