# HG changeset patch
# User wenzelm
# Date 1719927059 -7200
# Node ID 8f839104d460e790337d4b48b6222be6cebbd40e
# Parent  12901c03b416b21ad8610c0940213cc238d364cd
presumably unused (see also f992769dea97);

diff -r 12901c03b416 -r 8f839104d460 Admin/components/ci-extras
--- a/Admin/components/ci-extras	Mon Jul 01 18:22:33 2024 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-#components required for the CI infrastructure
-ci-extras-1