aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/dune
AgeCommit message (Expand)Author
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2020-11-13Fix dune rules for @check-gram following recent changes.Théo Zimmermann
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
2020-09-08Fix docgram's dune file following #12085.Théo Zimmermann
2020-03-30[dune] [docgram] Remove bash hack thanks to new option -no-update.Théo Zimmermann
2020-03-28New target check-gram to check if fullGrammar and orderedGrammar are up-to-date.Théo Zimmermann
2020-03-12Dune build rules for doc_grammar and fullGrammar.Théo Zimmermann