Skip to content

DuplicateFreeList: Make documentation more precise - #6625

Merged
fingolfin merged 1 commit into
gap-system:masterfrom
TWiedemann:tw/doc-duplicatefreelist
Sep 29, 2026
Merged

fingolfin merged 1 commit into
gap-system:masterfrom
TWiedemann:tw/doc-duplicatefreelist

Conversation

@TWiedemann

Copy link
Copy Markdown
Contributor

Clarifies how the order of the entries in DuplicateFreeList(oldList) is determined.

This came up here, where it matters in which order some files are scanned: gap-packages/AutoDoc#382

Text for release notes

none.

@fingolfin fingolfin added topic: documentation Issues and PRs related to documentation release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes labels Sep 29, 2026
@fingolfin
fingolfin merged commit 848c776 into gap-system:master Sep 29, 2026
31 checks passed
@codecov

codecov Bot commented Sep 29, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 79.23%. Comparing base (b2ebc4f) to head (a34c47c).
⚠️ Report is 1 commits behind head on master.

Additional details and impacted files
@@           Coverage Diff           @@
##           master    #6625   +/-   ##
=======================================
  Coverage   79.23%   79.23%           
=======================================
  Files         683      683           
  Lines      295181   295185    +4     
  Branches     8647     8647           
=======================================
+ Hits       233892   233898    +6     
+ Misses      59471    59470    -1     
+ Partials     1818     1817    -1     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@TWiedemann
TWiedemann deleted the tw/doc-duplicatefreelist branch September 29, 2026 11:52
cdwensley pushed a commit that referenced this pull request Oct 1, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes topic: documentation Issues and PRs related to documentation

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants