Fri, 15 Apr 2016 15:08:43 +0200 | wenzelm | clarified PIDE reports; | changeset | files |
Fri, 15 Apr 2016 14:27:59 +0200 | wenzelm | clarified rendering wrt. hyperlinks; | changeset | files |
Fri, 15 Apr 2016 13:02:23 +0200 | wenzelm | tuned -- no position; | changeset | files |