ci: allow to deploy docs manually (#14042)

This commit is contained in:
Julien Robert
2022-11-28 15:23:29 +01:00
committed by GitHub
parent 41f0ab15e6
commit 5ea5d91861
2 changed files with 2 additions and 1 deletions
+1
View File
@@ -2,6 +2,7 @@ name: Deploy docs
# This job builds and deploys documenation to github pages.
# It runs on every push to main with a change in the docs folder.
on:
workflow_dispatch:
push:
branches:
- main