diff options
| author | Dmitry Petrashko <dmitry.petrashko@gmail.com> | 2015-02-18 15:54:52 +0100 |
|---|---|---|
| committer | Dmitry Petrashko <dmitry.petrashko@gmail.com> | 2015-03-18 10:52:32 +0100 |
| commit | 8e3240b43a839506c71c8793f4d904c089918389 (patch) | |
| tree | eb0a0de8ee3136c7c7421cdc02270f4aaeff3a17 /.gitignore | |
| parent | ab24bcf84d64e5d6fa2201056f70fe38a3260cc1 (diff) | |
| download | dotty-8e3240b43a839506c71c8793f4d904c089918389.tar.gz dotty-8e3240b43a839506c71c8793f4d904c089918389.tar.bz2 dotty-8e3240b43a839506c71c8793f4d904c089918389.zip | |
Handle boxing inside labels, jump back to box.
Erasure inserts boxing and unboxing of label returned values, ignoring the fact that some labels do not return.
Now this is taken into account also inside labels which refer labels themselves
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions