mirror of https://github.com/seL4/docs.git
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>
This commit is contained in:
parent
6a3efa7f58
commit
c11f41c622
|
@ -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"
|
||||
|
|
Loading…
Reference in New Issue