Stream: Coq devs & plugin devs

Topic: ✔ What's up with coq_lsp in CI?


view this post on Zulip Rodolphe Lepigre (Jun 08 2024 at 13:32):

I'm getting a weird error here: https://gitlab.inria.fr/coq/coq/-/jobs/4420261.

view this post on Zulip Gaëtan Gilbert (Jun 08 2024 at 13:34):

https://github.com/rlepigre/coq_lsp not found

view this post on Zulip Gaëtan Gilbert (Jun 08 2024 at 13:34):

maybe private repo?

view this post on Zulip Rodolphe Lepigre (Jun 08 2024 at 13:41):

OK, I was stupid, it is coq-lsp, not coq_lsp in the URL. I messed up the overlay file.

view this post on Zulip Notification Bot (Jun 08 2024 at 13:42):

Rodolphe Lepigre has marked this topic as resolved.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 08 2024 at 14:40):

The underline thing is so annoying, but that's a limitation of our toolchain


Last updated: Oct 13 2024 at 01:02 UTC