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

fix(pkg): remove External_copy #10512

Merged
merged 1 commit into from
May 13, 2024
Merged

Conversation

rgrinberg
Copy link
Member

@rgrinberg rgrinberg commented May 10, 2024

Make it the same as file://. Both of these constructors mean the same thing, so let's keep one of them. This simplification also fixes dune reacting to changes made to pinned packages.

There's still some ugliness around the types. In particular, we should be more careful about where we expect the url to point to a file vs a directory.

Note that I still haven't yet removed the separate constructors in the frontend. That's going to conflict with some PR's I have, so I will do that later.

Signed-off-by: Rudi Grinberg me@rgrinberg.com

Make it the same as file://. Both of these constructors mean the same
thing, so let's keep one of them.

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

<!-- ps-id: cc26aabc-5ed3-42c9-90db-53efae6ec9da -->
@rgrinberg rgrinberg force-pushed the ps/rr/fix_pkg___remove_external_copy branch from 426a6a5 to 79b7df5 Compare May 13, 2024 15:52
@rgrinberg rgrinberg merged commit 0c50085 into main May 13, 2024
27 of 28 checks passed
@rgrinberg rgrinberg deleted the ps/rr/fix_pkg___remove_external_copy branch May 13, 2024 16:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants