Stream: Coq devs & plugin devs

Topic: make doc_gram


view this post on Zulip Enrico Tassi (Feb 09 2022 at 17:22):

Is the doc accurate? Can't I run it with dune?

view this post on Zulip Gaëtan Gilbert (Feb 09 2022 at 17:25):

please clarify

view this post on Zulip Théo Zimmermann (Feb 09 2022 at 17:28):

No, the doc is outdated. Gaëtan has made it so that make -f Makefile.dune also imports the same doc_gram targets as Makefile.make (though they still rely on make).

view this post on Zulip Théo Zimmermann (Feb 09 2022 at 17:29):

Please report or fix the doc issues that you've spotted.


Last updated: Feb 05 2023 at 21:03 UTC