From 0a06a3812ad3b7f2013690953d7d6b374f0e2476 Mon Sep 17 00:00:00 2001
From: Markus Schmidt <markus262@web.de>
Date: Thu, 23 Nov 2023 14:55:16 +0100
Subject: [PATCH] trigger ci

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

diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml
index 4971045293d..f613c5c9e24 100644
--- a/.github/workflows/gh-pages.yml
+++ b/.github/workflows/gh-pages.yml
@@ -66,13 +66,13 @@ jobs:
           git config --local user.name "github-actions[bot]"
 
       # sanitive head_ref name
-      - run: echo "DOC_VERSION_NAME=$(echo ${{ github.head_ref }} | sed "s/[^[:alnum:]-]//g" )" >> $GITHUB_ENV
+      - run: echo "DOC_VERSION_NAME=$(echo ${{ github.head_ref }} | sed "s/[^[:alnum:]-]/_/g" )" >> $GITHUB_ENV
 
 
 
       # on push to develop branch - keep a doc around for develop to show the current state
       - name: deploy doc in subdirectory
-        if: github.event_name == 'push'
+        if: github.event_name == 'push'se
         run: mike deploy develop
 
       # on PR events..
@@ -98,7 +98,7 @@ jobs:
       # sanitive head_ref name
       - name: sanitize tag name
         if: github.event_name == 'release'
-        run: echo "DOC_VERSION_NAME=${github.ref_name//[^[:alnum:]]/_}" >> $GITHUB_ENV
+        run: echo "DOC_VERSION_NAME=$(echo ${{ github.ref_name }} | sed "s/[^[:alnum:]-]/_/g" )" >> $GITHUB_ENV
 
       - name: deploy doc in subdirectory
         if: github.event_name == 'release'