diff options
| author | Maxime Dénès | 2015-10-16 13:20:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-10-16 13:36:04 +0200 |
| commit | d1ce79ce293c9b77f2c6a9d0b9a8b4f84ea617e5 (patch) | |
| tree | c21862745b135776c5d9b603d858fe04c045cf21 /kernel/nativelambda.mli | |
| parent | 4dd61c9459a7388078bbd2e1b6f07959c4c72001 (diff) | |
Remove left2right reference from the kernel.
Was introduced by seemingly unrelated commit
fd62149f9bf40b3f309ebbfd7497ef7c185436d5.
The currently policy is to avoid exposing global references in the kernel
interface when easily doable.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions