WIP: allowing ddocs deploy manual trigger

ibois-epfl · Dec 30, 2024 · 8ff77c9 · 8ff77c9
1 parent 5aa112d
commit 8ff77c9
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/.github/workflows/doc-build.yml b/.github/workflows/doc-build.yml
@@ -15,6 +15,8 @@ on:
       - 'deps/**'
       - 'docs/**'
       - 'materials/**'
+  workflow_dispatch: # allows manual trigger
+
 
 jobs:
   build-doc: