summaryrefslogtreecommitdiff
path: root/descr
AgeCommit message (Collapse)Author
2018-04-26Add a new SHARE_DIR argument to use when doing opam build. For non-opam ↵Robert Norton
builds this defaults to git root.