Run CI on dev branch

Having a `dev` branch is useful on occasion to commit stuff outside of a PR (but still not directly to `master`)
JuliaDocs · Nov 5, 2023 · 6f29e5b · 6f29e5b
1 parent fc68ab7
commit 6f29e5b
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -3,6 +3,7 @@ on:
   push:
     branches:
       - master
+      - dev
       - 'release-*'
     tags:
       - '*'