diff options
| author | Pierre-Marie Pédrot | 2018-05-27 17:58:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-27 18:06:18 +0200 |
| commit | cdae19b9eeb82f979c38de0047cdb4c5c2466e0c (patch) | |
| tree | cd21d86db089453552166cb41061dbb47c041568 /dev | |
| parent | b2f746e41abf53fc481f90804ba4d70edd73fc86 (diff) | |
Simplify the code that handles trust of side-effects in kernel typing.
For some reason the code was returning int option when only the value of
the integer was relevant.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions