diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2013-12-28 20:54:06 -0500 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2013-12-28 20:56:29 -0500 |
commit | 651094ccfd2d8106a8b0e75c27dc89afb369d4b3 (patch) | |
tree | 05cb006d7ed738758c9ae57883316dbc64c04a6a /kernel/nativelambda.ml | |
parent | d3eac3d5fc8e5af499eb8750ca08ead8562dac6f (diff) |
Revert "Partial revert of r16711"
The sharing introduced by this commit is now correct, since a reference used by
the native compiler has been removed from constant_body.
This reverts commit 413f5fcd4bf581ff3ea4694c193d637589c7d54f.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions