diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-19 14:05:52 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:12:47 +0200 |
commit | 906b48ff401f22be6059a6cdde8723b858102690 (patch) | |
tree | 0254ba66d050474ff0507dc0302d1da3b0d40024 /plugins | |
parent | 665256fec8465ff0adb943063c25f07a6ca54618 (diff) |
Avoiding a variable shadowing in the kernel.
This ought to ease the understanding of the code.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions