Skip to content

Bump JamesIves/github-pages-deploy-action from 4.5.0 to 4.6.0 #117

Bump JamesIves/github-pages-deploy-action from 4.5.0 to 4.6.0

Bump JamesIves/github-pages-deploy-action from 4.5.0 to 4.6.0 #117

Workflow file for this run

on:
pull_request_target:
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
jobs:
show_doc_diff:
timeout-minutes: 30
runs-on: ubuntu-latest
permissions:
pull-requests: write
contents: read
steps:
- uses: actions/setup-java@99b8673ff64fbf99d8d325f52d9a5bdedb8483e9 # v4.2.1
with:
java-version: 8
distribution: temurin
- uses: actions/checkout@9bb56186c3b09b4f86b1c65136769dd318469633 # v4.1.2
with:
ref: ${{ github.event.pull_request.head.sha }}
- name: Install pandoc
run: ./.github/install_pandoc.sh
- uses: coursier/cache-action@142d2738bd29f0eb9d44610828acb3a19809feab # v6.4.6
- name: Generate html
run: ./.github/gen_doc.sh
- uses: actions/checkout@9bb56186c3b09b4f86b1c65136769dd318469633 # v4.1.2
with:
ref: gh-pages
path: gh-pages
- run: |
cp -r target/specs2-reports/site/* gh-pages/
pushd gh-pages
git checkout -- javascript
git diff > diff.txt
wc -l diff.txt
popd
- uses: actions/github-script@v7
with:
script: |
const fs = require('fs');
const diff = fs.readFileSync("gh-pages/diff.txt").toString();
if (diff.length === 0) {
console.log("no diff");
} else {
github.rest.issues.createComment({
issue_number: context.issue.number,
owner: context.repo.owner,
repo: context.repo.repo,
body: "```diff\n" + diff + "\n```"
});
}