Skip to content

Update to version v0.0.18 #102

Update to version v0.0.18

Update to version v0.0.18 #102

Workflow file for this run

name: GitHub CI
# Controls when the workflow will run
on:
# Triggers the workflow on push events for the main branch
push:
branches: [ main ]
# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:
# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
# This workflow contains a single job called "build"
build:
# The type of runner that the job will run on
runs-on: ubuntu-latest
# Steps represent a sequence of tasks that will be executed as part of the job
steps:
# Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
- uses: actions/checkout@v4
# Run the report
- name: Run coverage report
run: ./coverage.sh -d .
# Write index file
- name: Create index.html
run: |
cat << EOF > ./reports/index.html
<html lang="en-US">
<head>
<meta charset="UTF-8">
<meta http-equiv="refresh" content="0; url=/specification-tests/coverage">
<script type="text/javascript">
window.location.href = "/specification-tests/coverage"
</script>
<title>Page Redirection</title>
</head>
<body>
If you are not redirected automatically, follow this <a href='/specification-tests/coverage'>link to the coverage report.</a>.
</body>
</html>
EOF
# Deploy the report to GitHub pages
- name: Deploy
uses: peaceiris/actions-gh-pages@v3
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
publish_dir: ./reports
user_name: 'github-actions[bot]'
user_email: 'github-actions[bot]@users.noreply.github.com'