Allow manually triggering a documentation build.

gouttegd · gouttegd · commit 4e4576b597ef · 2025-02-12T22:52:43.000Z
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -3,6 +3,7 @@ name: Build and publish the documentation
 on:
   push:
     branches: [ "main" ]
+  workflow_dispatch:
 
 jobs:
   build:
