deploy on push

Author: Massimiliano Pippi

Diff for: .github/workflows/docs.yaml

@@ -2,10 +2,6 @@ name: docs
 
 on:
   pull_request:
-    types:
-      - opened
-      - synchronize
-      - closed
     paths:
       # existing docs
       - 'docs/**'
@@ -15,6 +11,15 @@ on:
       - 'cli/**'
       # potential changes to gRPC documentation
       - 'rpc/**'
+  push:
+    branches:
+      - master
+    # At this day, GitHub doesn't support YAML anchors, d'oh!
+    paths:
+      - 'docs/**'
+      - 'docsgen/**'
+      - 'cli/**'
+      - 'rpc/**'
 
 jobs:
   build:
@@ -67,8 +72,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 }}

Diff for: docs/index.md

@@ -22,4 +22,4 @@ interface of the CLI. Available services and messages are detailed in the
 [installation]: installation.md
 [Getting started guide]: getting-started.md
 [client_example]: https://github.com/arduino/arduino-cli/blob/master/client_example
-[gRPC reference]: rpc/commands
+[gRPC reference]: rpc/commands