diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-02 22:34:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-02 22:34:30 +0200 |
| commit | fb406f8b33014c63139bbafd472b6afe7a4f72c9 (patch) | |
| tree | d1f6e4a9b93ed51953d98a4970d7aeb89c83d020 /Makefile.ci | |
| parent | 04756f75bf54b1ccda8c180c62b14c5eaaaabb67 (diff) | |
| parent | d19d296c2b584954e9adb97eed7c705cc1db4bc7 (diff) | |
Merge PR #7680: [ci] Expose updated `OCAMLPATH` for CI users.
Diffstat (limited to 'Makefile.ci')
0 files changed, 0 insertions, 0 deletions