echo $COV_NUM > gwion-coverage-report/coverage_num.txt
sed -i 's/<html>/<script type="text\/javascript" src="focus.js"><\/script><html>/' index.src_*.html
branch=$(basename ${{ github.event.ref }})
+ gcovr --filter '.*\.c$' src > lines.txt
+ gcovr --filter '.*\.c$' --branches src > branches.txt
cd gwion-coverage-report/
bash old.sh $branch
bash summary.sh
- cd ..
- gcovr --filter '.*\.c$' src > gwion-coverage-report/html/$branch/lines.txt
- gcovr --filter '.*\.c$' --branches src > gwion-coverage-report/html/$branch/branches.txt
- mv *.html gwion-coverage-report/html/$branch
- name: Make badge
if: github.event_name == 'push' && github.event.ref == 'refs/heads/master'
cd gwion-coverage-report
bash badge.sh
- - name: Push Report
- if: github.event_name == 'push'
+ - name: git config
+ if: github.event_name == 'push' && github.event.ref == 'refs/heads/master'
run: |
cd gwion-coverage-report
git config --local user.email "action@github.com"
git config --local user.name "GitHub Action"
git remote set-url origin https://${{ secrets.COVERAGE_TOKEN }}@github.com/fennecdjay/gwion-coverage-report.git
+
+ - name: Push Report
+ if: github.event_name == 'push' && github.event.ref == 'refs/heads/master'
+ run: |
+ cd gwion-coverage-report
git add README.md coverage_num.txt
git commit -m "Update coverage" || true
git push || true
- git push origin :gh-pages || true
+
+ - name: Push Pages
+ if: github.event_name == 'push'
+ run: |
+ cd gwion-coverage-report
+ rm -r html
+ mv *.html *.txt gwion-coverage-report/html/$branch
cp focus.js html
git add -f html
git commit -m "Update html report"
projects / gwion.git / commitdiff