workflow_dispatch added to be able to trigger the build of the docs manually

Paulchen-Panther · Paulchen-Panther · commit ea194170ca46 · 2025-06-12T09:30:45.000+02:00
diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
@@ -1,5 +1,6 @@
 name: Documentation CI Build
 on:
+  workflow_dispatch:
   push:
     branches-ignore:
       - 'gh-pages'
