From 6ea15c30b8928c3d72b18028426c9c4bd7f0bd7c Mon Sep 17 00:00:00 2001
From: Mirko Bunse <mirko.bunse@cs.tu-dortmund.de>
Date: Mon, 24 Jun 2024 14:19:13 +0200
Subject: [PATCH] TO REVERT: build gh-pages even on pushes to devel

---
 .github/workflows/ci.yml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 7fcecff..0cd88ba 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -36,7 +36,6 @@ jobs:
   docs:
     name: Documentation
     runs-on: ubuntu-latest
-    if: github.ref == 'refs/heads/master'
     steps:
     - uses: actions/checkout@v1
     - name: Build documentation