Skip to content

Conversation

grunweg
Copy link
Collaborator

@grunweg grunweg commented May 2, 2025

This script repeats the same logic for all ~5 different emojis now: extract the logic into short functions to make the code shorter.


Commits are best reviewed individually.

Open in Gitpod

@grunweg grunweg added the CI Modifies the continuous integration setup or other automation label May 2, 2025
Copy link

github-actions bot commented May 2, 2025

PR summary f17197c039

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 2, 2025
@grunweg grunweg force-pushed the MR-dedup-emoji-merge-delegate branch from cf54236 to 0d36030 Compare May 2, 2025 11:58
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 2, 2025
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@bryangingechen
Copy link
Contributor

Not sure from the discussion in Zulip if this is still being tested but LGTM.
bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 2, 2025

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@grunweg
Copy link
Collaborator Author

grunweg commented May 2, 2025

I would say: yes, this is being tested - but the logic change is orthogonal to this refactoring, so let's land this first. Thanks for the quick review!
bors r+

mathlib-bors bot pushed a commit that referenced this pull request May 2, 2025
…24545)

This script repeats the same logic for all ~5 different emojis now: extract the logic into short functions to make the code shorter.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 2, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor(zulip-emoji-merge-delegate.py): consolidate repeated logic [Merged by Bors] - refactor(zulip-emoji-merge-delegate.py): consolidate repeated logic May 2, 2025
@mathlib-bors mathlib-bors bot closed this May 2, 2025
@mathlib-bors mathlib-bors bot deleted the MR-dedup-emoji-merge-delegate branch May 2, 2025 14:08
pfaffelh pushed a commit that referenced this pull request May 2, 2025
…24545)

This script repeats the same logic for all ~5 different emojis now: extract the logic into short functions to make the code shorter.
riccardobrasca pushed a commit that referenced this pull request May 7, 2025
…24545)

This script repeats the same logic for all ~5 different emojis now: extract the logic into short functions to make the code shorter.
tannerduve pushed a commit that referenced this pull request May 13, 2025
…24545)

This script repeats the same logic for all ~5 different emojis now: extract the logic into short functions to make the code shorter.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

CI Modifies the continuous integration setup or other automation delegated

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants