diff options
| author | Pierre-Marie Pédrot | 2019-06-24 19:05:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-26 12:38:27 +0200 |
| commit | 64e66fd019b968f863a80d4bce972545a66ea966 (patch) | |
| tree | 97d120af900084eb7e4113c44e9372ee6a9defa8 /kernel/cemitcodes.ml | |
| parent | 6fab6f1cbf21d6f4a3a77e1b73c31fbe18d05a11 (diff) | |
Perform the opaque section variable inference outside of the kernel.
It is not the role of the kernel to decide to force the body of an entry
to infer the section variable it uses, but the one of the upper layers.
We make this explicit in the type of entries so as to enforce that this
inference is performed beforehand.
Also removes auxilliary file stuff that doesn't look like it belongs in
the kernel either.
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions