aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGuillaume Melquiond2015-12-26 10:07:19 +0100
committerGuillaume Melquiond2015-12-31 17:01:51 +0100
commit1a157442dff4bfa127af467c49280e79889acde7 (patch)
tree7d10a0093e75b652c7cce79920c054d4c2f41c91 /kernel
parent1a8a8db7a9e4eb5ab56cd192411529661a4972c7 (diff)
Do not compose List.length with List.filter.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions