Merge pull request #24 from ltratt/move_to_ghmqs

Move to GitHub merge queues.
softdevteam · Nov 9, 2023 · 22b5e02 · 22b5e02
2 parents e2c68d4 + 6224e80
commit 22b5e02
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 8 deletions.
diff --git a/.github/workflows/sdci.yml b/.github/workflows/sdci.yml
@@ -0,0 +1,11 @@
+on:
+  pull_request:
+  merge_group:
+
+# This is required to silence emails about the workflow having no jobs.
+# We simply define a dummy job that does nothing much.
+jobs:
+  dummy:
+    runs-on: ubuntu-latest
+    steps:
+      - run: /usr/bin/true
diff --git a/bors.toml b/bors.toml