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