diff options
| author | Maxime Dénès | 2018-02-12 10:00:00 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-12 10:00:00 +0100 |
| commit | 8e048ebb124416448156dbfade1b7f826828e466 (patch) | |
| tree | 9718f600f4f5ff7ace211199c7139744ef8cafff /kernel/nativelib.ml | |
| parent | 4fb4f1adf18648b4fb561986379e033b00423148 (diff) | |
| parent | f12a980ad7136440210de1d275f909cc9dfb6fe4 (diff) | |
Merge PR #6706: ci-common: guess CI_BRANCH for local builds
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions