[opam-devel] Automatically synching GitHub pulls to OPAM
thomas.gazagnaire at gmail.com
Fri Feb 7 16:37:15 GMT 2014
> I can publish this regularly as a custom remote, but it occurs to me that during the 6-month GitHub experiment, we may as well merge this directly into OPAM stable. Most users will not see all the extra repositories due to requiring the --all script.
I think that's a great idea, but would be nice to automatically remove closed PRs though if we do this.
Also, not sure how to handle the PR which adds / modifies the configure options, but we could fix that later.
More information about the opam-devel