Wed, 09 Apr 2014 15:03:07 +0200 | wenzelm | more explicit message discrimination; | changeset | files |
Wed, 09 Apr 2014 13:32:34 +0200 | wenzelm | avoid confusion about pointless cursor movement with external links; | changeset | files |
Wed, 09 Apr 2014 12:33:02 +0200 | wenzelm | prefer regular Goal_Display.pretty_goals, without censorship of options; | changeset | files |
Wed, 09 Apr 2014 12:28:24 +0200 | wenzelm | more standard names; | changeset | files |