Allow manual deployment of the developer guides (#3155)

IgnatBeresnev · web-flow · commit 61619d5b7946 · 2023-09-01T16:49:11.000+02:00
diff --git a/.github/workflows/gh-pages-deploy-dev-docs.yml b/.github/workflows/gh-pages-deploy-dev-docs.yml
@@ -1,6 +1,7 @@
 name: Deploy developer docs to GitHub Pages
 
 on:
+  workflow_dispatch:
   push:
     branches:
       - master
