From 5a320baa45b8e826e52bdd6cadadfad727ab0357 Mon Sep 17 00:00:00 2001 From: David Robertson Date: Thu, 28 Apr 2022 11:31:26 +0100 Subject: [PATCH] changelog --- changelog.d/12576.misc | 1 + 1 file changed, 1 insertion(+) create mode 100644 changelog.d/12576.misc diff --git a/changelog.d/12576.misc b/changelog.d/12576.misc new file mode 100644 index 0000000000..71022c8633 --- /dev/null +++ b/changelog.d/12576.misc @@ -0,0 +1 @@ +Allow unused `#type: ignore` comments in bleeding edge CI jobs.