while true
do wget https://badgen.net/badge/coverage/$COV_NUM/$COLOR -O gwion-coverage-report/badge.svg && break
done
+ sed -i 's/<html>/<script type="text\/javascript" src="focus.js"><\/script><html>/' index.src_*.html
branch=$(basename ${{ github.event.ref }})
mkdir -p gwion-coverage-report/html/$branch
mv *.html gwion-coverage-report/html/$branch
git commit -m "Update coverage" || true
git push || true
cp focus.js html
- sed -i 's/<html>/<script type="text\/javascript" src="focus.js"><\/script><html>/' html/index.src_*.html
git add -f html
git commit -m "Update html report"
git push origin :gh-pages || true
projects / gwion.git / commitdiff