Stream: Dune devs & users

Topic: Pending PR on plugins


view this post on Zulip Emilio Jesús Gallego Arias (Sep 02 2022 at 15:19):

Hi @Ali Caglayan , can we discuss here about https://github.com/ocaml/dune/pull/5968 to unblock it? (Or over zoom)

view this post on Zulip Emilio Jesús Gallego Arias (Sep 02 2022 at 15:19):

I'm unsure what the problem is, as the change to deps is wrong, I feel that maybe there is some misunderstanding on how plugins work on Coq?

view this post on Zulip Ali Caglayan (Sep 02 2022 at 15:26):

Hi @Emilio Jesús Gallego Arias, we can discuss it.

view this post on Zulip Ali Caglayan (Sep 02 2022 at 15:26):

Over zoom would be good I think, since i haven't been able to describe my intention with it so well.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 02 2022 at 15:27):

Sounds good


Last updated: Jan 30 2023 at 18:04 UTC