From b1414b2a043706cb85589e8ea7a5b8ca95672189 Mon Sep 17 00:00:00 2001
From: Mirko Bunse <mirko.bunse@cs.tu-dortmund.de>
Date: Mon, 24 Jun 2024 15:05:49 +0200
Subject: [PATCH] Revert "TO REVERT: build gh-pages even on pushes to devel"
This reverts commit 6ea15c30b8928c3d72b18028426c9c4bd7f0bd7c.
---
.github/workflows/ci.yml | 1 +
1 file changed, 1 insertion(+)
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index fc7c805..b1e275c 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -36,6 +36,7 @@ jobs:
docs:
name: Documentation
runs-on: ubuntu-latest
+ if: github.ref == 'refs/heads/master'
steps:
- uses: actions/checkout@v1
- name: Build documentation