Skip to content

Merge branch 'stefan/jaeger_wip' into 'master' #115

Merge branch 'stefan/jaeger_wip' into 'master'

Merge branch 'stefan/jaeger_wip' into 'master' #115

# This workfow makes sure the gitlab-mirror branch is always in sync with the master branch
name: GitLab Sync Branches
on:
push:
branches:
- master
workflow_dispatch:
jobs:
sync-branches:
runs-on: ubuntu-latest
if: ${{ vars.RUN_CI == 'true' }}
steps:
- name: Checkout
uses: actions/checkout@v3
with:
fetch-depth: 0
token: ${{ secrets.GH_CI_TOKEN }}
- name: Setup Git User
run: |
git config user.name "GitHub Actions Bot"
git config user.email "[email protected]"
# Normally this would fail, as branch protection rules only allow merging via a PR
# But we gave sa-github-api a custom role that allows bypassing branch rules and use its PAT for this job
- name: Update mirroring branch
run: |
git fetch origin master mirroring
git checkout -B mirroring
git rebase --onto master origin/mirroring
git push origin mirroring --force-with-lease