Deploy docs when a release is made

Author: mpickering

.github/workflows/build.yaml

@@ -1,5 +1,5 @@
 name: Build
-on: [push, pull_request]
+on: [push, pull_request, release]
 jobs:
   build:
     runs-on: ubuntu-latest
@@ -52,7 +52,7 @@ jobs:
     - run: find build-folder -type d -exec chmod 755 {} \;
     - run: find build-folder -type f -exec chmod 644 {} \;
     - name: Deploy to GitHub Pages
-      if: github.event_name == 'create' && github.event.ref_type == 'tag'
+      if: github.event_name == 'release'
       uses: JamesIves/github-pages-deploy-action@releases/v3
       with:
         BRANCH: gh-pages