merge queue: checking main (191035e) and #2058 together - #2059
mergify[bot] wants to merge 16 commits into
Conversation
Copy make_metrics_datasets.py aside before checking out the data-only metrics-history branch, then write output/ next to aggregated/*.json in the same commit.
The newer metrics-history snapshots store compile_memory_usage alongside the text report. Rank top RSS files from that array, attach peak_rss_mb to compile_times, and strip CI workspace prefixes from labels.
Add a push input to upload_metrics_history and call it from on PR with push: false so the datasets are built without updating the orphan branch.
|
Thanks @mergify[bot] for opening this PR! You can do multiple things directly here: Once the workflow completes a message will appear displaying informations related to the run. Also the PR gets automatically reviewed by gemini, you can: |
Workflow reportworkflow report corresponding to commit 67d681c Pre-commit check reportPre-commit check: ✅ Test pipeline can run. Clang-tidy diff reportNo relevant changes found. You should now go back to your normal life and enjoy a hopefully sunny day while waiting for the review. Doxygen diff with
|
🎉 This pull request has been checked successfully and will be merged soon. 🎉
Branch main (191035e) and #2058 are queued together for merge.
This pull request has been created by Mergify to check the mergeability of #2058.
You don't need to do anything. Mergify will close this pull request automatically when it is complete.
Required conditions of queue rule
main queuefor merge:check-success = allRequired conditions to stay in the queue:
approved-reviews-by >= 1check-success = all_lightcheck-success = pre-commit.ci - pr