diff options
| author | Pierre-Marie Pédrot | 2015-05-19 19:36:31 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-19 19:36:31 +0200 |
| commit | 5a52a74592496353d562d9f3e958fb59ab585531 (patch) | |
| tree | bb1e7ac53b8ff60a51ef7efab050540da0b5acd0 /kernel/nativecode.ml | |
| parent | d5c1f2133a80304ce8a1890e3568b14fafd8f283 (diff) | |
Adding an extensible global state to evarmaps.
Evars already had their own extensible state, but adding it globally allows
to write out extensible state-passing code in e.g. plugins. The additional
data is hopefully transparently preserved by the code out there. Trespassers
ought to be prosecuted.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions