Tue, 06 May 2014 16:05:14 +0200 | wenzelm | explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts"; | changeset | files |
Tue, 06 May 2014 15:54:22 +0200 | wenzelm | tuned GUI layout; | changeset | files |