| Sun, 08 Oct 2017 16:50:37 +0200 | wenzelm | more on Docker; | changeset | files |
| Sun, 08 Oct 2017 15:54:55 +0200 | wenzelm | removed obsolete RC tags; | changeset | files |
| Sun, 08 Oct 2017 14:52:06 +0200 | wenzelm | build_docker is regular tool (non-admin); | changeset | files |