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

Feature/mini repo #2257

Closed
wants to merge 2 commits into from
Closed

Feature/mini repo #2257

wants to merge 2 commits into from

Conversation

bobot
Copy link
Contributor

@bobot bobot commented Jul 15, 2015

Fix the poblem with virtual package in #2098. The side effect is that archive/*.virtual files are now created by opam mk-repo but it seems not bad.

@bobot
Copy link
Contributor Author

bobot commented Jul 15, 2015

@perrelle is currently testing more thoroughly the patch.

@AltGr
Copy link
Member

AltGr commented Jul 17, 2015

A simpler/cleaner way could be to add an option to opam-admin to restrict the packages directly, rather than do it through a shell-script (and require a separate channel for packages without archives): something like opam-admin make --resolve-and-filter <packages> that turns a full repository into a limited one only for the listed packages.

@samoht
Copy link
Member

samoht commented Jan 18, 2016

Any update on this? I could use it :-)

@ghost ghost mentioned this pull request Jan 27, 2016
Closed
@AltGr AltGr added this to the Next milestone Aug 31, 2016
@AltGr
Copy link
Member

AltGr commented May 2, 2017

We now have a clean way to do this, using opam admin filter :)

@AltGr AltGr closed this May 2, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
AREA: REPOSITORY KIND: FEATURE WISH STATE: WAITING FOR FEEDBACK
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@bobot @AltGr @samoht