Closed JasonGross closed 2 years ago
It seems that the step is no longer needed on newer versions of opam, so the docs should mention that this step is only required on opam < 2.1
Does opam-depext
still work (without the previous step) or did the syntax change?
We have a related issue that the platform scripts are broken with opam 2.1 (coq/platform#116). It would be convenient if it could be fixed by just skipping the broken step in case opam >= 2.1 is detected.
[Transferring to the relevant repo since it's a website issue]
BTW, if you know what to change, feel free to open a PR. The relevant file is: https://github.com/coq/www/blob/master/pages/opam-using.html
Does
opam-depext
still work (without the previous step) or did the syntax change?
No, there is no opam-depext
anymore, it happens automatically with opam install
.
It would be convenient if it could be fixed by just skipping the broken step in case opam >= 2.1 is detected.
Yes, we can just skip the opam depext steps in this case, as long as we can pass "y" to the relevant prompt.
Description of the problem
https://coq.inria.fr/opam-using.html says
However, the first command gives