aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-06-20 08:14:28 +0200
committerPierre-Marie Pédrot2019-06-24 11:02:11 +0200
commitbbec0ea51b4dfef1ddb09a2f876323aa1547f643 (patch)
tree137c8e3c1d5cb05815e393fdf024b11dfe517d77 /dev/ci
parentbe3bba54e39a316ded975b7c5ac5723fed41aa88 (diff)
Dedicated type for opaque entries in the kernel.
Even more invariants can be enforced this way.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions