From 646bdc5a008a4ce42514c54af736d1d2784b6ce0 Mon Sep 17 00:00:00 2001 From: Guido Berning <30648231+SaJaToGu@users.noreply.github.com> Date: Mon, 20 Jul 2026 19:41:30 +0200 Subject: [PATCH] ci: track dev instead of develop after branch rename develop was renamed to dev on GitHub for consistency with metis and odysseus. Update the push/pull_request triggers so CI still runs on the active development branch. --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4253c6a..f4703dc 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -4,11 +4,11 @@ on: push: branches: - main - - develop + - dev pull_request: branches: - main - - develop + - dev workflow_dispatch: jobs: