aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-05 13:19:54 +0100
committerPierre-Marie Pédrot2018-11-05 13:19:54 +0100
commit5202b20739d18137780b7729ee657b7eecef5c0c (patch)
treededf81cdb23cc530db04a6bfe1a42528397afdb3 /dev/ci
parent538a54e8855d477e9ca350a76f852a147809a06b (diff)
parentf18ea56a697fe27467e499d35495e18b866de371 (diff)
Merge PR #8866: Check universe instances in Typing
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions