Stream: Coq devs & plugin devs

Topic: ✔ Make -f Makefile.dune default

view this post on Zulip Ali Caglayan (Feb 13 2022 at 21:09):

Was there a way to make Makefile.dune the default? I couldn't find anything in the docs

view this post on Zulip Ali Caglayan (Feb 13 2022 at 21:18):

Oh ok found it

view this post on Zulip Ali Caglayan (Feb 13 2022 at 21:18):

There is an env var COQ_USE_DUNE

view this post on Zulip Notification Bot (Feb 14 2022 at 14:09):

Ali Caglayan has marked this topic as resolved.

Last updated: Jun 09 2023 at 08:01 UTC