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

diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
index 087eca6d00536aea8861d5a4f4a3050967a5ba48..9115cd3ef6f4555fe24e8512207cf269c8dfbad4 100644 (file)
--- a/.github/workflows/coverage.yml
+++ b/.github/workflows/coverage.yml
@@ -74,8 +74,8 @@ jobs:
         git commit -m "Update coverage" || true
         git push || true
         cp focus.js html
-        git add -f html
         sed -i 's/<html>/<script type="text\/javascript" src="focus.js"><html>/' html/index.src_*.html
+        git add -f 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