run build_docs on pull request (#664)

Summary:


# Context
Pull requests don't run build docs command, so if that breaks it is only seen after commit lands

# This Diff
1. Makes build docs job run on all pull requests
2. creates sub job for publish that only runs on commit (so it won't publish docs for every pull request)

Reviewed By: galrotem

Differential Revision: D52379374

.github/workflows/build_docs.yaml

@@ -3,6 +3,7 @@ name: Build and Update Docs
 on:
   push:
     branches: [ master ]
+  pull_request:
 
 # Allow one concurrent deployment
 concurrency:
@@ -40,6 +41,10 @@ jobs:
           make html
           touch build/html/.nojekyll
           cd ..
+  publish_docs:
+    runs-on: ubuntu-latest
+    if: ${{ github.event_name == 'push' }}
+    steps:
       - name: Deploy docs to Github pages
         uses: JamesIves/github-pages-deploy-action@v4.4.1
         with: