Ignore dependabot pushes correctly

dependabot opens a branch in the main repository and then opens a pull
request, which triggers the same build twice. To avoid that, we had
branches-ignore set to ignore the push.

However the syntax was incorrect: since the branch name contains
slashes, we have to use two stars to ignore it. See [0] for details on
that syntax.

[0]: https://docs.github.com/en/actions/reference/workflow-syntax-for-github-actions#filter-pattern-cheat-sheet

.github/workflows/ci.yml

@@ -3,7 +3,7 @@ name: CI
 on:
   push:
     branches-ignore:
-      - "dependabot/*"
+      - "dependabot/**"
   pull_request:
 
 jobs: