Skip to content

Merge branch 'main' into ricardomiron-patch-5 #514

Merge branch 'main' into ricardomiron-patch-5

Merge branch 'main' into ricardomiron-patch-5 #514

Workflow file for this run

# The only reason this CI exists is that we can require branches to be up
# to date before merging, which can only be enforced if there is at least
# one status check enabled.
name: Dummy CI
on:
push:
pull_request:
jobs:
dummy:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- name: Dummy action
run: echo dummy