diff options
| author | Gaëtan Gilbert | 2020-04-13 15:16:09 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-13 15:16:09 +0200 |
| commit | 0beca74bc90cef03d779a8e4f8668335c9c37716 (patch) | |
| tree | ceba4106f623f8e62474c7ea985f5214c4f580eb /kernel/section.ml | |
| parent | 1a309cd7d8547d9a2b5ee89adfe8ba1c581237e1 (diff) | |
| parent | 646a12b2f4660d6e9d5a812febdccab44221d1f0 (diff) | |
Merge PR #12087: Temporarily disable Windows job on Azure.
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/section.ml')
0 files changed, 0 insertions, 0 deletions