| Tue, 01 Oct 2019 19:08:24 +0200 | wenzelm | obsolete (see 60abd1e94168); | changeset | files |
| Tue, 01 Oct 2019 11:42:23 +0200 | wenzelm | more robust after shutdown; | changeset | files |
| Tue, 01 Oct 2019 11:29:03 +0200 | wenzelm | more sequential access to Session.manager.global_state: avoid minor divergence of tip version; | changeset | files |