aboutsummaryrefslogtreecommitdiff
path: root/ide/dune-workspace
AgeCommit message (Expand)Author
2018-10-05[dune] Refactor files following advice from upstream.Emilio Jesus Gallego Arias
2018-10-05[ci] [dune] [opam] Fixes to OPAM and CI target.Emilio Jesus Gallego Arias