docs: add workflow_dispatch

Enables manual dispatch for building the docs, as desired for `dev`.
This is necessary as only workflows registered in the default branch
with `workflow_dispatch` can be triggered from the GitHub interface.

.github/workflows/docs.yml

@@ -3,6 +3,7 @@ name: docs
 
 # execute this workflow automatically when we push to master
 on:
+  workflow_dispatch:
   push:
     branches:
       - master