aboutsummaryrefslogtreecommitdiff
path: root/.github/workflows
diff options
context:
space:
mode:
authorIgnat Beresnev <ignat.beresnev@jetbrains.com>2023-09-01 16:49:11 +0200
committerGitHub <noreply@github.com>2023-09-01 16:49:11 +0200
commit61619d5b794616678934d4de89fb08857c293225 (patch)
tree8b167b3a22f70b5f29d0cc7d080cfcb55414ceca /.github/workflows
parent32c88d525de89de1d0d055b2fa65b5cd48ccaec3 (diff)
downloaddokka-61619d5b794616678934d4de89fb08857c293225.tar.gz
dokka-61619d5b794616678934d4de89fb08857c293225.tar.bz2
dokka-61619d5b794616678934d4de89fb08857c293225.zip
Allow manual deployment of the developer guides (#3155)
Diffstat (limited to '.github/workflows')
-rw-r--r--.github/workflows/gh-pages-deploy-dev-docs.yml1
1 files changed, 1 insertions, 0 deletions
diff --git a/.github/workflows/gh-pages-deploy-dev-docs.yml b/.github/workflows/gh-pages-deploy-dev-docs.yml
index 9b4fdb52..ce1caf35 100644
--- 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