From c11f41c6228fd9540bfd4055b2d69b9ac52ed4d4 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Wed, 16 Jul 2025 10:05:37 +1000
Subject: [PATCH] inject_backlink: make GNU sed compatible

BSD sed allows a space after -i, GNU sed does not.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 tools/inject_backlink.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/inject_backlink.sh b/tools/inject_backlink.sh
index d0c182353e..182a889978 100755
--- a/tools/inject_backlink.sh
+++ b/tools/inject_backlink.sh
@@ -19,4 +19,4 @@ TOC="$1/toc.js"
 
 LINK='<li style="margin-top: 3rem;" class="part-title"><a href="../">Back to seL4 docsite</a>'
 
-sed -i .bak "s|</li></ol>|</li>${LINK}</ol>|" "$TOC"
+sed -i.bak "s|</li></ol>|</li>${LINK}</ol>|" "$TOC"