Wed, 02 May 2012 21:55:13 +0200 | wenzelm | makedist for release; | changeset | files |
Wed, 02 May 2012 21:23:14 +0200 | wenzelm | merged | changeset | files |
Wed, 02 May 2012 21:21:51 +0200 | wenzelm | more contributors; | changeset | files |
Wed, 02 May 2012 21:15:38 +0200 | wenzelm | tuned latex sources; | changeset | files |
Wed, 02 May 2012 21:15:15 +0200 | wenzelm | more CHECKLIST; | changeset | files |
Wed, 02 May 2012 20:57:59 +0200 | wenzelm | save 90MB by removing foreign binaries -- multi-platform installations are unlikely on Windows; | changeset | files |
Wed, 02 May 2012 20:43:57 +0200 | wenzelm | some re-ordering; | changeset | files |