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.

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

Error when multiple dev-repos collide on dir #377

Merged
merged 2 commits into from
Feb 22, 2023

Commits on Feb 21, 2023

  1. Error when multiple dev-repos collide on dir

    The duniverse directory of a package is implied by its dev-repo. It's
    possible for different dev-repos to map to the same directory. Prior to
    this change, one lucky package would be downloaded to the expected place
    and the others would be silently ignored. More precisely, each package
    would be downloaded and placed in the duniverse dir implied by their
    dev-repo, but first any existing duniverse dir of the same name would be
    removed.
    
    After this change, the same situation results in an error when running
    `opam monorepo lock`.
    
    Signed-off-by: Stephen Sherratt <stephen@sherra.tt>
    gridbugs committed Feb 21, 2023
    Configuration menu
    Copy the full SHA
    ad48b0c View commit details
    Browse the repository at this point in the history

Commits on Feb 22, 2023

  1. Configuration menu
    Copy the full SHA
    c658448 View commit details
    Browse the repository at this point in the history