Admin/components/ci-extras
author lammich <lammich@in.tum.de>
Fri, 02 Jun 2017 09:26:04 +0200
changeset 66005 10e5265c2a25
parent 63143 ef72b104fa32
permissions -rw-r--r--
merged

#components required for the CI infrastructure
ci-extras-1