Merge branch 'master' of github.com:ethanmsl/rename_files

.github/workflows/web.yml

@@ -10,6 +10,8 @@ permissions:
 # All of these work independently and can be removed / commented out
 # if you don't want oranda/mdbook running in that situation
 on:
+  # allow manual run of this workflow
+  workflow_dispatch:
   # Check that a PR didn't break docs!
   #
   # Note that the "Deploy to Github Pages" step won't run in this mode,
@@ -96,4 +98,4 @@ jobs:
           # Gotta tell the action where to find oranda's output
           folder: public
           token: ${{ secrets.GITHUB_TOKEN }}
-          single-commit: true
+          single-commit: true