From 0f5ae593bea7314184608a32122da73ed559f219 Mon Sep 17 00:00:00 2001 From: Johannes Schindelin Date: Sat, 21 May 2022 22:18:51 +0000 Subject: [PATCH] ci: optionally mark up output in the GitHub workflow A couple of commands exist to spruce up the output in GitHub workflows: https://docs.github.com/en/actions/learn-github-actions/workflow-commands-for-github-actions In addition to the `::group::