Skip to content

chore: use new HashMap in allNamesByModule#14523

Merged
adomani merged 1 commit intonightly-testingfrom
name_hashmap
Jul 8, 2024
Merged

chore: use new HashMap in allNamesByModule#14523
adomani merged 1 commit intonightly-testingfrom
name_hashmap

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Jul 8, 2024

Note this is a PR to nightly-testing, since this isn't available on master yet, but I think it can be reviewed normally.

@kim-em kim-em requested a review from TwoFX July 8, 2024 16:52
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 8, 2024

PR summary 060c2d88bd

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Too many changes (264)!

Declarations diff

- get!_none
- get!_some
- isSome_map

You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Jul 8, 2024

@adomani the declarations diff appears to be incorrect, here. Do we need to disable this for PRs to something other than master?

@adomani
Copy link
Copy Markdown
Contributor

adomani commented Jul 8, 2024

The script already takes an optional commit that defaults to master. I would have to look into how to make the action detect the target branch and the script can run with that instead of master, I suppose.

I won't have time to look at it today, though, as I'm about to have dinner!

@adomani adomani merged commit 1c3b03d into nightly-testing Jul 8, 2024
@mathlib-bors mathlib-bors bot deleted the name_hashmap branch July 8, 2024 19:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants