Escape slashes in sed command

sfauvel · sfauvel · commit 7807895f015a · 2024-07-31T14:12:01.000+02:00
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -910,7 +910,7 @@ jobs:
           echo "mithril.network" > ./github-pages/CNAME
           echo '<!DOCTYPE html><html><head><meta http-equiv="Refresh" content="0; URL=https://mithril.network/doc"></head></html>' > ./github-pages/index.html
           # Remove the index.html from the url to avoid a display issue that duplicates the content of the page
-          sed -i '1s/^/<script type="text/javascript"> if (window.location.href.endsWith("/index.html")) { end_of_clean_url = window.location.href.lastIndexOf("/"); window.location.href = window.location.href.substring(0, end_of_clean_url); } </script>\n/' ./github-pages/doc/index.html
+          sed -i '1s/^/<script type="text\/javascript"> if (window.location.href.endsWith("\/index.html")) { end_of_clean_url = window.location.href.lastIndexOf("\/"); window.location.href = window.location.href.substring(0, end_of_clean_url); } <\/script>\n/' ./github-pages/doc/index.html
 
       - name: Mithril / Publish GitHub Pages
         uses: peaceiris/actions-gh-pages@v3
