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

diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
index db1b712d7296a347b06f7dd294261559cc753659..f43c1353a478650cf16ecbd252100147d9d1e425 100644 (file)
--- a/.github/workflows/coverage.yml
+++ b/.github/workflows/coverage.yml
@@ -73,10 +73,9 @@ jobs:
         git add README.md coverage_num.txt
         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/index.src_*.html
         git commit -m "Update html report"
         git push origin :gh-pages || true
         git subtree push --prefix html origin gh-pages
-        git rm -r html
-        git commit -m "Update coverage" || true
-        git push || true
strongly-timed musical programming language