aboutsummaryrefslogtreecommitdiff
path: root/dev/incdir
AgeCommit message (Collapse)Author
2019-02-18[dev] Add include versions for Dune builds.Emilio Jesus Gallego Arias
Fixes #9537 This way, users can do: ``` dune exec coqtop.byte > Drop. # #directory "dev";; # #use "include_dune";; ```