Fri, 01 Jan 2016 11:27:29 +0100 | wenzelm | clarified abbrev; | changeset | files |
Fri, 01 Jan 2016 11:18:54 +0100 | wenzelm | clarified meaning of \<^bold> action, depending on group; | changeset | files |
Fri, 01 Jan 2016 11:12:43 +0100 | wenzelm | clarified groups, notably for Symbols dockable; | changeset | files |