deploy on push

Author: Massimiliano Pippi

.github/workflows/docs.yaml

@@ -1,12 +1,18 @@
 name: docs
 
+paths:
+  # existing docs
+  - 'docs/**'
+  # changes to the cli reference generator
+  - 'docsgen/**'
+  # potential changes to commands documentation
+  - 'cli/**'
+  # potential changes to gRPC documentation
+  - 'rpc/**'
+
 on:
   pull_request:
-    types:
-      - opened
-      - synchronize
-      - closed
-    paths:
+    paths: &p
       # existing docs
       - 'docs/**'
       # changes to the cli reference generator
@@ -15,6 +21,11 @@ on:
       - 'cli/**'
       # potential changes to gRPC documentation
       - 'rpc/**'
+  push:
+    branches:
+      - master
+    paths:
+      <<: *p
 
 jobs:
   build:
@@ -67,8 +78,8 @@ jobs:
         run: task docs:build
 
       - name: Deploy
-        # publish docs only when PR is merged
-        if: github.event.pull_request.merged == true
+        # publish docs only when PR is merged on master
+        if: github.event_name == 'push'
         uses: peaceiris/actions-gh-pages@v3
         with:
           github_token: ${{ secrets.GITHUB_TOKEN }}