Trigger workflow on pull requests

kgryte · kgryte · commit f9c40b13f559 · 2021-08-18T19:24:48.000-07:00
diff --git a/.github/workflows/repl_docs.yml b/.github/workflows/repl_docs.yml
@@ -21,9 +21,11 @@ name: repl_docs
 
 # Workflow triggers:
 on:
-  push:
+  pull_request:
     branches:
       - develop
+    types:
+      - closed
     paths:
       # List paths for which changes should trigger this workflow:
       - 'lib/**/namespace/lib/**'
@@ -44,6 +46,9 @@ jobs:
     # Define a display name:
     name: 'Update REPL docs'
 
+    # Only run this job if the pull request was merged:
+    if: github.event.pull_request.merged == true
+
     # Define the type of virtual host machine:
     runs-on: ubuntu-latest
 
