Hi folks, this is a warning that we will bump the minimal required dune version for a full dev dune build to 2.9.2 soon
What does "full dev build" mean? (Will make world
still work fine with dune 2.7.0?)
Full dev build is the build method using Dune for vo files, as opposed to the "hybrid" / legacy one.
I.e., the one relying on Makefile.dune
as opposed to Makefile.make
Did you manage to get the deps right? That would be awesome!
Last updated: Jun 08 2023 at 04:01 UTC