diff options
| author | Gaëtan Gilbert | 2020-04-16 19:43:45 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-16 19:43:45 +0200 |
| commit | 4bf8191357007fac41199d91c7f7a2c4870f323f (patch) | |
| tree | 86c23e1f067de88fca84dd590b5965f6987f5b8c /kernel/nativelambda.ml | |
| parent | d2d55a710b26e48c94b3241077f30938c1ffb5e8 (diff) | |
| parent | 4055a45e2fa436bbffbab5b1a6b0271581f563da (diff) | |
Merge PR #12069: [gitlab-ci] Only run Windows jobs when ONLY_WINDOWS variable is true.
Reviewed-by: gares
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions