Admin/components/ci-extras
author wenzelm
Wed, 15 Jul 2020 12:43:36 +0200
changeset 72037 aa6a36c730c9
parent 63143 ef72b104fa32
permissions -rw-r--r--
proper platform path for Windows;

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