| Mon, 29 Jun 2015 21:56:20 +0200 | wenzelm | clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c); | changeset | files |
| Mon, 29 Jun 2015 20:55:46 +0200 | wenzelm | improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded); | changeset | files |