From 6ff17eaab8aad54bcb3d79055846c27ca0251fcc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois?= <mockersf@gmail.com>
Date: Tue, 15 Mar 2022 23:52:44 +0000
Subject: [PATCH] Deploy dev docs - fix sed command (#4221)

# Objective

- #3535 introduced deploying docs with an error in sed command

## Solution

- fix sed command
- make the command cross platform
---
 .github/workflows/docs.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index e471a81330..d8dd7f7644 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -28,7 +28,7 @@ jobs:
       #   - Adds a meta tag that forces Google not to index any page on the site.
       - name: Pre-docs-build
         run: |
-          sed -i "s/icon.png/icon-docs-dev.png" src/lib.rs
+          sed -i.bak "s/icon.png/icon-docs-dev.png/" src/lib.rs
           echo "<meta name=\"robots\" content=\"noindex\">" > header.html
 
       - name: Build docs