Skip to content

chore(Condensed): shorten some names#17140

Closed
dagurtomas wants to merge 2 commits intomasterfrom
dagur/LocallyConstantGolf2
Closed

chore(Condensed): shorten some names#17140
dagurtomas wants to merge 2 commits intomasterfrom
dagur/LocallyConstantGolf2

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented Sep 25, 2024

Open in Gitpod

dagurtomas
dagurtomas commented Sep 25, 2024
View reviewed changes
@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 25, 2024 •
edited
Loading

PR summary da40831a3c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ functorIso
+ functorToPresheavesIso
- functorIsoTopCatToSheafCompHausLike
- functorToPresheavesIsoTopCatToSheafCompHausLike

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.

@dagurtomas dagurtomas mentioned this pull request Sep 25, 2024
Closed
vihdzp
vihdzp reviewed Sep 25, 2024
View reviewed changes
@dagurtomas dagurtomas closed this Sep 25, 2024
@YaelDillies YaelDillies deleted the dagur/LocallyConstantGolf2 branch August 15, 2025 16:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@vihdzp vihdzp vihdzp left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@dagurtomas @vihdzp