[opam-devel] Automatically synching GitHub pulls to OPAM

[Thomas Gazagnaire]

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.

--
Thomas