Re-amalgamate single_include (#5745)

* Re-amalgamate single_include

#5737 changed 13 headers under include/ but merged without the matching
single_include/nlohmann/json.hpp update, so the amalgamated header still
had, among others, the GCC C++20 -Wignored-attributes pragma block and
the clang -Wdocumentation push/pop that #5737 removed, the forwarding
from_json tuple/array helpers it replaced with const references, and
lacked the output_adapter char_traits changes it added.

Regenerated with `make amalgamate` (astyle 3.4.13). The diff is exactly
`git diff b54ed188e e5a89d671 -- include/` (164+/95-); json_fwd.hpp and
json_literals.hpp were already up to date.

Signed-off-by: Niels Lohmann <mail@nlohmann.me>

* Run the amalgamation check on pushes to develop

#5737 was merged 39 seconds after its last push, while its own
check_amalgamation run was still queued (earlier runs had been
cancelled by the concurrency group), so the stale single_include
reached develop without any failing check.

Also run the check on pushes to develop, without cancelling in-progress
develop runs. The "save" job (PR number/author for the comment
workflow) only runs for pull requests, the checkout falls back to
github.sha, and comment_check_amalgamation.yml only comments for
PR-triggered runs, since push runs have no PR and no "pr" artifact.

Signed-off-by: Niels Lohmann <mail@nlohmann.me>

---------

Signed-off-by: Niels Lohmann <mail@nlohmann.me>
This commit is contained in:
Niels Lohmann
2026-10-01 08:09:34 +02:00
committed by GitHub
parent e5a89d671f
commit e400780533
3 changed files with 176 additions and 99 deletions

View File

@@ -2,16 +2,23 @@ name: "Check amalgamation"
on:
pull_request:
# also check develop itself: a PR can be merged before its own run of this
# workflow completes (e.g. while it is still queued), leaving single_include
# stale on develop without any failing check
push:
branches:
- develop
concurrency:
group: ${{ github.workflow }}-${{ github.ref || github.run_id }}
cancel-in-progress: true
cancel-in-progress: ${{ github.event_name == 'pull_request' }}
permissions:
contents: read
jobs:
save:
if: github.event_name == 'pull_request'
runs-on: ubuntu-latest
steps:
- name: Harden Runner
@@ -43,11 +50,11 @@ jobs:
with:
egress-policy: audit
- name: Checkout pull request
- name: Checkout pull request or pushed commit
uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
with:
path: main
ref: ${{ github.event.pull_request.head.sha }}
ref: ${{ github.event.pull_request.head.sha || github.sha }}
persist-credentials: false
- name: Checkout tools

View File

@@ -10,7 +10,8 @@ permissions:
jobs:
comment:
if: ${{ github.event.workflow_run.conclusion == 'failure' }}
# push runs on develop have no PR to comment on (and no "pr" artifact)
if: ${{ github.event.workflow_run.conclusion == 'failure' && github.event.workflow_run.event == 'pull_request' }}
runs-on: ubuntu-latest
permissions:
contents: read