aboutsummaryrefslogtreecommitdiff
path: root/tools/dune
diff options
context:
space:
mode:
authorEnrico Tassi2018-10-10 18:09:38 +0200
committerEnrico Tassi2018-10-10 18:09:38 +0200
commit040ad198e38776bb9f398329243b2fe41434f2d5 (patch)
tree51547819395d4f6798a9c2368c85fb521e820657 /tools/dune
parentea38cc10b1b3d81e2346de6b95076733ef4fd7bb (diff)
parent95f751136ba3a8f8c2544d8d7d48125c52030836 (diff)
Merge PR #8692: [test-suite] Don't reset `OCAMLPATH`, but append to it.
Diffstat (limited to 'tools/dune')
0 files changed, 0 insertions, 0 deletions