diff options
| author | Pierre Letouzey | 2015-11-29 01:05:06 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2015-12-12 18:51:37 +0100 |
| commit | e2915d2e615a271c90d9e8c8599a428ed15828b5 (patch) | |
| tree | da69e5d6178aff08caf52b0dd5bf57a6d1a8222d /kernel/nativecode.mli | |
| parent | 5550d920b831ec080cac236840132770bf1ba754 (diff) | |
Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)
The ind_equiv field wasn't correctly set, due to some kernel names
glitches (canonical vs. user). The fix is to take into account the
delta_resolver while traversing module structures.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions