aboutsummaryrefslogtreecommitdiff
path: root/kernel/cPrimitives.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2020-04-17 14:32:02 +0200
committerThéo Zimmermann2020-04-17 14:32:02 +0200
commitf3af9a4c6e6813f32dfe632209e145ffbf5fed98 (patch)
tree44632df517b713a6bd487445e433dab9b9d98e16 /kernel/cPrimitives.ml
parent87f8c9fce73ebf8bc0b6cb53536bdb3861f09e41 (diff)
parent633b462dc0c0211d353faebc6acbe6393c1566b6 (diff)
Merge PR #12111: CI: Ignore spurious errors in validate jobs
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/cPrimitives.ml')
0 files changed, 0 insertions, 0 deletions