aboutsummaryrefslogtreecommitdiff
path: root/dune-workspace
AgeCommit message (Expand)Author
2018-10-05[dune] Refactor files following advice from upstream.Emilio Jesus Gallego Arias
2018-10-01Merge PR #8579: [dune] [merlin] Fix some usability issues.Maxime Dénès
2018-09-29[dune] Enable warning 60 [unused local module]Emilio Jesus Gallego Arias
2018-09-27[dune] [merlin] Fix some usability issues.Emilio Jesus Gallego Arias
2018-09-06[dune] [ci] Fix and test release profile + use 1.1 dune-workspaceEmilio Jesus Gallego Arias