|
|
name: Sync |
|
|
on: |
|
|
workflow_dispatch: |
|
|
push: |
|
|
branches: [ main, "release/**" ] |
|
|
pull_request: |
|
|
branches: [ main ] |
|
|
|
|
|
permissions: |
|
|
contents: read |
|
|
|
|
|
jobs: |
|
|
sync-autogenerated: |
|
|
|
|
|
|
|
|
|
|
|
name: Check autogenerated file freshness |
|
|
runs-on: ubuntu-latest |
|
|
permissions: |
|
|
contents: write |
|
|
steps: |
|
|
- name: Checkout |
|
|
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 |
|
|
with: |
|
|
submodules: false |
|
|
fetch-depth: 0 |
|
|
fetch-tags: false |
|
|
|
|
|
|
|
|
ref: ${{ github.event.pull_request.head.ref || github.ref }} |
|
|
repository: ${{ github.event.pull_request.head.repo.full_name || github.repository }} |
|
|
|
|
|
- name: UpdateDates |
|
|
if: | |
|
|
github.event_name != 'pull_request' && |
|
|
(startsWith(github.ref, 'refs/heads/release/') || |
|
|
startsWith(github.ref, 'refs/tags/pcre2-')) |
|
|
run: maint/UpdateDates.py |
|
|
|
|
|
- name: UpdateAlways |
|
|
run: maint/UpdateAlways |
|
|
|
|
|
- name: 'Rebuild *.h.generic' |
|
|
run: | |
|
|
./autogen.sh && ./configure |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
chmod u=rw,go=r m4/*.m4 |
|
|
|
|
|
rm -f src/*.generic |
|
|
make src/config.h.generic src/pcre2.h.generic |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- name: Commit and push, if not in a forked repo |
|
|
if: github.event_name != 'pull_request' || ( ! github.event.pull_request.head.repo.fork && github.actor != 'dependabot[bot]' ) |
|
|
run: | |
|
|
if [ -n "`git status --porcelain`" ] ; then |
|
|
# Dirty working tree: push it |
|
|
git config user.name "github-actions[bot]" |
|
|
git config user.email "41898282+github-actions[bot]@users.noreply.github.com" |
|
|
git add -u |
|
|
git commit -m "Sync autogenerated files #noupdate" |
|
|
git push |
|
|
fi |
|
|
|
|
|
sync-docs: |
|
|
name: Sync content from main to pages |
|
|
runs-on: ubuntu-latest |
|
|
if: github.event_name != 'pull_request' && github.ref == 'refs/heads/main' |
|
|
needs: ['sync-autogenerated'] |
|
|
permissions: |
|
|
contents: write |
|
|
steps: |
|
|
- name: Checkout |
|
|
uses: actions/checkout@1af3b93b6815bc44a9784bd300feb67ff0d1eeb3 |
|
|
with: |
|
|
submodules: false |
|
|
fetch-depth: 0 |
|
|
fetch-tags: false |
|
|
ref: pages |
|
|
|
|
|
- name: Commit and push, if docs have changed |
|
|
run: | |
|
|
if ! git diff --exit-code origin/main -- \ |
|
|
./doc ./AUTHORS.md ./LICENCE.md ./SECURITY.md ./README.md \ |
|
|
./README ./NON-AUTOTOOLS-BUILD >/dev/null ; then |
|
|
# Differences from main: merge and push |
|
|
git config user.name "github-actions[bot]" |
|
|
git config user.email "41898282+github-actions[bot]@users.noreply.github.com" |
|
|
git merge origin/main --no-edit -m"Sync content from main to pages" |
|
|
git push |
|
|
else |
|
|
echo "No content changes to sync" |
|
|
fi |