From 96126e7ce9d23c451b536c1f8e80a540b0489a69 Mon Sep 17 00:00:00 2001
From: flip1995 <philipp.krones@embecosm.com>
Date: Thu, 21 Oct 2021 18:00:57 +0200
Subject: [PATCH] Fix deploy script

I broke this script in #7502, so that the stable symlink isn't generated
anymore. This reverts this change.
---
 .github/deploy.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/deploy.sh b/.github/deploy.sh
index a3c57232f557..34225a540290 100644
--- a/.github/deploy.sh
+++ b/.github/deploy.sh
@@ -13,7 +13,8 @@ cp util/gh-pages/lints.json out/master
 if [[ -n $TAG_NAME ]]; then
   echo "Save the doc for the current tag ($TAG_NAME) and point stable/ to it"
   cp -Tr out/master "out/$TAG_NAME"
-  ln -sf "$TAG_NAME" out/stable
+  rm -f out/stable
+  ln -s "$TAG_NAME" out/stable
 fi
 
 if [[ $BETA = "true" ]]; then