]> Nishi Git Mirror - gwion.git/commitdiff
projects / gwion.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 4d7086c)
use js
authorJérémie Astor <astor.jeremie@wanadoo.fr>
Mon, 17 Feb 2020 20:12:11 +0000 (21:12 +0100)
committerJérémie Astor <astor.jeremie@wanadoo.fr>
Mon, 17 Feb 2020 20:12:11 +0000 (21:12 +0100)
.github/workflows/coverage.yml patch | blob | history

diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
index f43c1353a478650cf16ecbd252100147d9d1e425..087eca6d00536aea8861d5a4f4a3050967a5ba48 100644 (file)
--- a/.github/workflows/coverage.yml
+++ b/.github/workflows/coverage.yml
@@ -75,7 +75,7 @@ jobs:
         git push || true
         cp focus.js html
         git add -f html
-        sed -i 's/<html>/<script type="text/javascript" src="focus.js">/' html/index.src_*.html
+        sed -i 's/<html>/<script type="text\/javascript" src="focus.js"><html>/' html/index.src_*.html
         git commit -m "Update html report"
         git push origin :gh-pages || true
         git subtree push --prefix html origin gh-pages
strongly-timed musical programming language