Sat, 20 Jul 2013 16:18:17 +0200 | wenzelm | obscure options; | changeset | files |
Sat, 20 Jul 2013 16:16:23 +0200 | wenzelm | print_state at high priority -- fast and important; | changeset | files |
Fri, 19 Jul 2013 23:29:43 +0200 | wenzelm | proper Future.shutdown, to wait for the scheduler thread to finish remaining tasks (notably external processes); | changeset | files |