Stream: Dune devs & users

Topic: ✔ Dune for separate extraction


view this post on Zulip Li-yao (Apr 02 2024 at 21:35):

Thanks, omitting the modules field works!

view this post on Zulip Notification Bot (Apr 02 2024 at 21:35):

Li-yao has marked this topic as resolved.

view this post on Zulip Ali Caglayan (Apr 03 2024 at 08:29):

Currently the extracted_modules field doesn't support pforms, i.e. you cannot write %{include:foo} for some file foo with the names of the modules contrary to other fields we have in dune. This should be easy to implement and if you think it would be useful you can open an issue on github.


Last updated: May 25 2024 at 21:01 UTC