Sat, 09 Jan 2016 13:31:17 +0100 | wenzelm | tuned syntax; | changeset | files |
Sat, 09 Jan 2016 13:00:04 +0100 | wenzelm | tuned; | changeset | files |
Sat, 09 Jan 2016 12:58:57 +0100 | wenzelm | \<struct> loses its rendering and is superseded by \<diamondop>; | changeset | files |
Sat, 09 Jan 2016 12:35:07 +0100 | wenzelm | discontinued \<struct> syntax; | changeset | files |
Fri, 08 Jan 2016 20:06:48 +0100 | wenzelm | tuned whitespace; | changeset | files |
Fri, 08 Jan 2016 19:46:30 +0100 | wenzelm | tuned; | changeset | files |
Fri, 08 Jan 2016 18:18:40 +0100 | wenzelm | clarified symbol insertion, depending on buffer encoding; | changeset | files |