Ali Caglayan

@palmskog last I spoke to @ybertot he wanted to have a look at the readme in some more detail. So we are waiting for him.

Won't this also inherit the common flags like enabling and disabling promotion which are probably noops here.

Seems to be feature that users want, but neither I or the other devs care to implement at this time. There are a few pitfalls as Hugo suggested and I...

I would also prefer something like that. I don't remember why but I seem to recall there being some reservations about introducing a command line argument for a plugin.

@SkySkimmer That doesn't let build systems choose the extraction output directory however. My original motivation for this is so that we could get Dune to output Coq extracted files in...

@coqbot run full ci

I will run the full ci just in case. Note that we don't test coqdoc at all in the CI.

I also wouldn't mind any comments from @coq/coqdoc-maintainers.

@SkySkimmer I don't mean in the test-suite but in the other external projects. We definitely don't test all of the flags here in the test-suite.

@coqbot merge now