From 84bb35a3a1904f466c69f352b2ce33cb99071298 Mon Sep 17 00:00:00 2001
From: Wolfgang Walther <walther@technowledgy.de>
Date: Sun, 11 May 2025 12:20:07 +0200
Subject: [PATCH] labels: no CI label for OWNERS changes

We can use the same "hack" as in labeler-no-sync.yml, because OWNERS is
the only file without extension in that directory structure.

This makes it easier to search for CI related PRs via label.
---
 .github/labeler.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/labeler.yml b/.github/labeler.yml
index 03d218711774..7f1ac6d2ea32 100644
--- a/.github/labeler.yml
+++ b/.github/labeler.yml
@@ -39,7 +39,7 @@
     - changed-files:
       - any-glob-to-any-file:
         - .github/**/*
-        - ci/**/*
+        - ci/**/*.*
 
 "6.topic: coq":
   - any: