Skip to content

[Merged by Bors] - chore: remove duplicated namespaces from instances#10899

Closed
Ruben-VandeVelde wants to merge 2 commits intomasterfrom
dupns
Closed

[Merged by Bors] - chore: remove duplicated namespaces from instances#10899
Ruben-VandeVelde wants to merge 2 commits intomasterfrom
dupns

Conversation

@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor


Open in Gitpod

@digama0
Copy link
Copy Markdown
Member

digama0 commented Feb 24, 2024

We don't want this to fire on autogenerated instance names. Do you know whether that is possible or likely with this change?

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 24, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 25, 2024
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor Author

Note that this PR only contains the code changes, not the linter. I think we should land this regardless of what happens to the linter change.

@riccardobrasca
Copy link
Copy Markdown
Member

I agree the we have a separate problem, but this LGTM, thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Feb 28, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 28, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: remove duplicated namespaces from instances [Merged by Bors] - chore: remove duplicated namespaces from instances Feb 28, 2024
@mathlib-bors mathlib-bors bot closed this Feb 28, 2024
@mathlib-bors mathlib-bors bot deleted the dupns branch February 28, 2024 12:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants