Dispatch master-pushes to dev deployment. (#497)

.github/workflows/ci.yml

@@ -18,6 +18,9 @@ env:
   HAS_PROTOBUF: false
   RUN_TESTS: true
   ARTIFACT_EXTENSION: tgz
+  DEV_DEPLOYMENT_OWNER: toitware
+  DEV_DEPLOYMENT_REPO: web-docs-dev
+  DEV_DEPLOYMENT_WORKFLOW: ci.yml
 
 jobs:
   snippets:
@@ -104,6 +107,22 @@ jobs:
             ${{ env.VERSION }}.${{ env.ARTIFACT_EXTENSION }}
             VERSION
 
+      - name: Dispatch dev-deployment
+        if: github.ref == 'refs/heads/master'
+        uses: actions/github-script@v7
+        with:
+          github-token: ${{ secrets.LEON_REPOSITORY_DISPATCH }}
+          script: |
+            await github.rest.actions.createWorkflowDispatch({
+              owner: '${{ env.DEV_DEPLOYMENT_OWNER }}',
+              repo: '${{ env.DEV_DEPLOYMENT_REPO }}',
+              workflow_id: '${{ env.DEV_DEPLOYMENT_WORKFLOW }}',
+              ref: 'main',
+              inputs: {
+                'run-id': '${{ github.run_id }}',
+              },
+            });
+
   deploy:
     if: |
       github.event.inputs.deploy == 'true' ||