sync-github-prs.yaml

## %CopyrightBegin%
##
## Copyright Ericsson AB 2024. All Rights Reserved.
##
## Licensed under the Apache License, Version 2.0 (the "License");
## you may not use this file except in compliance with the License.
## You may obtain a copy of the License at
##
##     http://www.apache.org/licenses/LICENSE-2.0
##
## Unless required by applicable law or agreed to in writing, software
## distributed under the License is distributed on an "AS IS" BASIS,
## WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
## See the License for the specific language governing permissions and
## limitations under the License.
##
## %CopyrightEnd%

name: Sync all github prs with erlang.github.io/prs/

## Sync all github prs twice a day
on:
  workflow_dispatch:
  schedule:
  ## In UTC
  - cron: '0 */4 * * *'

permissions:
  contents: read

jobs:

  sync-prs:
    if: github.repository == 'erlang/otp'
    concurrency: erlang.github.io-deploy
    runs-on: ubuntu-20.04
    steps:
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # ratchet:actions/checkout@v4.2.2
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # ratchet:actions/checkout@v4.2.2
        with:
          token: ${{ secrets.ERLANG_TOKEN }}
          repository: 'erlang/erlang.github.io'
          path: erlang.github.io
      - name: Update PRs
        env:
          GITHUB_TOKEN: ${{secrets.GITHUB_TOKEN}}
        run: |
            git clone https://github.com/talentdeficit/jsx
            (cd jsx && rebar3 compile)
            mkdir -p "${GITHUB_WORKSPACE}/erlang.github.io/prs/"
            touch "${GITHUB_WORKSPACE}/erlang.github.io/.nojekyll"
            .github/scripts/sync-github-prs.es erlang/otp "${GITHUB_WORKSPACE}/erlang.github.io/prs/"

      - name: Deploy to github pages 🚀
        run: |
          cd erlang.github.io
          set -x
          git config user.name github-actions
          git config user.email github-actions@github.com
          git add .
          git add -u
          git update-index --refresh
          if ! git diff-index --quiet HEAD --; then
            git commit -m "Update github pages content"
            git push origin master
          fi