Merge pull request #4 from cidrblock/add_gate_merge

Add gate merge

.github/workflows/merge_on_gate.yml

@@ -0,0 +1,34 @@
+name: Merge a pull request
+on:
+  pull_request:
+    branches:
+    - main
+    types: [labeled]
+
+jobs:
+  merge:
+    if: |
+      github.event.label.name == 'gate'
+    name: merge
+    runs-on: ubuntu-latest
+    steps:
+    - name: Install gh
+      run: |
+        sudo apt-key adv --keyserver keyserver.ubuntu.com --recv-key C99B11DEB97541F0
+        sudo apt-add-repository https://cli.github.com/packages
+        sudo apt update
+        sudo apt install gh
+   
+    - name: Check out code
+      uses: actions/checkout@v2
+      with:
+        fetch-depth: 0
+
+    - name: Checkout default branch and merge PR
+      env:
+        DEFAULT_BRANCH: ${{ github.event.repository.default_branch }}
+        PR: ${{ github.event.number }}
+        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      run: |
+        git checkout $DEFAULT_BRANCH
+        gh pr merge $PR --squash