Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Check that the repositories given to "opam repository remove" actually exist #5014

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Check that the repositories given to "opam repository remove" actually exist #5014

wants to merge 3 commits into from

Conversation

kit-ty-kate
Copy link
Member

Fixes #5012

@rjbou rjbou added the PR: WIP Not for merge at this stage label Jan 20, 2022
rjbou
rjbou reviewed Jan 20, 2022
View reviewed changes
src/client/opamCommands.ml Outdated Show resolved Hide resolved
@rjbou rjbou self-assigned this May 18, 2022
@rjbou rjbou force-pushed the check-repos-remove-exist branch from d0cde13 to 6a0b06e Compare May 18, 2022 12:26
@rjbou rjbou self-requested a review January 23, 2023 13:47
@kit-ty-kate kit-ty-kate added PR: NEEDS UPDATE and removed PR: WIP Not for merge at this stage labels Jul 10, 2024
@kit-ty-kate kit-ty-kate added this to the 2.3.0~alpha milestone Jul 10, 2024
@kit-ty-kate
Copy link
Member Author

I've put back my original changes together with fixes to what needed fixing together with a couple of new tests.

Your original wip commit was 6a0b06e, i've also tried to improve the previous attempt in check-repos-remove-exist-old to no avail.
Given the increase of complexity of solutions that do not use ref i don't think it's worth demonizing references for such a local and non-performance-cricical use, and I think this work is ready to be reviewed and merged.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@rjbou rjbou Awaiting requested review from rjbou

At least 1 approving review is required to merge this pull request.

Assignees

@rjbou rjbou

Labels
AREA: UI
Projects
None yet
Milestone
2.4.0~alpha1
Development

Successfully merging this pull request may close these issues.

Confused by opam remote remove when remote does not exist
2 participants
@kit-ty-kate @rjbou