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 · 7f64cca · 7f64cca
1 parent b8064cc
commit 7f64cca
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:
       - '*'