Paolo Giarrusso (Nov 12 2020 at 21:21): Paolo Giarrusso (Nov 12 2020 at 21:21):Since coq.inria.fr is down, I wanted to redirect coq-released to read from https://github.com/coq/opam-coq-archive/tree/master/released. But I don't see how to do it. Some variations I tried:
opam repo set-url -v coq-released git+https://github.com/coq/opam-coq-archive/released#master # fails
opam repo set-url coq-released git+https://github.com/coq/opam-coq-archive.git#master # finds the wrong folder
Does anybody have a solution? Or would one need a "subrepository" for just the released folder? I could just move the files in a branch and point to that one
Gaëtan Gilbert (Nov 12 2020 at 21:29):you can clone locally and point opam at your clone
this does mean update is a 2-step git pull + opam update instead of just opam update
Paolo Giarrusso (Nov 12 2020 at 21:30):okay, branch created:
opam repo set-url coq-released git@github.com:Blaisorblade/opam-coq-archive.git#released
seems to work
Paolo Giarrusso (Nov 12 2020 at 21:31):I'm not entirely sure about the license of the result, but everything else seems fine.
Paolo Giarrusso (Nov 12 2020 at 21:32):good point on the local clone, hadn't thought of that. That URL is easier for now (no upgrades planned once the website is back up).
Last updated: Oct 13 2024 at 01:02 UTC