From 3ba9ae637cd8827e2936ffe95b66084e9ddfd920 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 12 Jan 2021 12:36:17 +0100 Subject: [PATCH] Run doxygen deploy on push and do not keep history --- .github/workflows/doxygen.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/doxygen.yml b/.github/workflows/doxygen.yml index d7b5c9396..26aecd93b 100644 --- a/.github/workflows/doxygen.yml +++ b/.github/workflows/doxygen.yml @@ -2,6 +2,9 @@ name: Doxygen # Builds and deploys storms doxygen documentation on: + push: + branches: + - master # needed to trigger the workflow manually workflow_dispatch: @@ -45,3 +48,4 @@ jobs: publish_dir: ./html external_repository: moves-rwth/storm-doc publish_branch: master + force_orphan: true