[opam-devel] Automatically synching GitHub pulls to OPAM

Thomas Gazagnaire thomas.gazagnaire at gmail.com
Fri Feb 7 16:37:15 GMT 2014

That's awesome!!!

> 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 mailing list