-
Notifications
You must be signed in to change notification settings - Fork 162
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
Removing remove directive #703
Comments
I'm definitely in favor of advising people not to use them. However, for the "huge PR", I would defer to @gares if that's advisable with CI. Maybe CI could be circumvented for the PR? |
Another aspect of this removal that should be mentioned: a lot of knowledge about logical paths will be lost. Ideally, one would process and remove:
and at the same time add |
Indeed it would be nice to turn these remove instructions into a logpath metadata. It is a good idea. I'm afraid I did not advise package authors to do that, but we should. Wrt the pr, I'm ok with it if it turns the fields into a logpath metadata. But beware il will be a lot of work, while it will naturally happen if we are strict with pr reviews. Maybe we should just improve the linting check. |
* feat: Add build for mathcomp/mathcomp-dev:coq-8.10 * fix(coq-mathcomp-ssreflect.opam): Bump coq upper bound * fix(*.opam): Remove "remove" directive href: coq/opam#703
For packages I'm maintaining. c.f. coq#703
In many packages there are the directives:
However, with opam 2, these are not necessary any more. In many PR reviews it was advised to remove them. Is there a policy about these directives? Should we remove all of them?
I would be in favor of:
remove
/light-uninstall
instances at once.The text was updated successfully, but these errors were encountered: