From d172010e5288cd34fea0b150acba4393f76246ab Mon Sep 17 00:00:00 2001 From: Niels de Vos Date: Mon, 24 Aug 2020 09:29:17 +0200 Subject: [PATCH] ci: add script to fetch labels for GitHub PR By passing `--id=` the labels of the given Pull-Request or Issue get printed. When adding `--has-label=