From af8cab7e5c3b0bdba625b169b02b95f1aeab9652 Mon Sep 17 00:00:00 2001
From: Markus Schmidt <markus262@web.de>
Date: Tue, 31 Oct 2023 14:49:02 +0100
Subject: [PATCH] trigger ci

---
 .github/workflows/gh-pages.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml
index 7d99ad75a9a..17b0f05f463 100644
--- a/.github/workflows/gh-pages.yml
+++ b/.github/workflows/gh-pages.yml
@@ -46,8 +46,8 @@ jobs:
           git config --local user.name "github-actions[bot]"
 
       - name: deploy doc in subdirectory
-        run: mike deploy ${{ github.ref }} --push
+        run: mike deploy $(echo ${{ github.event.ref }} | sed -e "s#refs/heads/##g") --push
 
       - name: deploy doc and update alias 'latest' to the new doc deployment
         if: github.event_name == 'release' && github.event.action == 'created'
-        run: mike --push --update-aliases ${{ github.ref }} latest
\ No newline at end of file
+        run: mike --push --update-aliases $(echo ${{ github.event.ref }} | sed -e "s#refs/heads/##g") latest
\ No newline at end of file