Sun, 08 Oct 2017 14:52:06 +0200 build_docker is regular tool (non-admin);
wenzelm [Sun, 08 Oct 2017 14:52:06 +0200] rev 66790
build_docker is regular tool (non-admin);
Sun, 08 Oct 2017 14:48:47 +0200 merged
wenzelm [Sun, 08 Oct 2017 14:48:47 +0200] rev 66789
merged
Sun, 08 Oct 2017 11:58:01 +0200 Added tag Isabelle2017 for changeset 64b47495676d
wenzelm [Sun, 08 Oct 2017 11:58:01 +0200] rev 66788
Added tag Isabelle2017 for changeset 64b47495676d
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 tip