diff options
author | Dmitry Petrashko <dark@d-d.me> | 2016-07-01 11:49:38 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-07-01 11:49:38 +0200 |
commit | 07fd8a357ed660ef15163efb2788928fec290fdd (patch) | |
tree | b5d358272bf0edc109e5e84cfa18822f31562b61 /src/dotty/tools/dotc/core | |
parent | b35eff93fd6ad23bc2ac2ee81952c435a7a90961 (diff) | |
parent | 7f43e4918715330c1407d5723ce73d023ca4229c (diff) | |
download | dotty-07fd8a357ed660ef15163efb2788928fec290fdd.tar.gz dotty-07fd8a357ed660ef15163efb2788928fec290fdd.tar.bz2 dotty-07fd8a357ed660ef15163efb2788928fec290fdd.zip |
Merge pull request #1350 from dotty-jvican/issue-1308
Add straightforward fix to #1308
Diffstat (limited to 'src/dotty/tools/dotc/core')
0 files changed, 0 insertions, 0 deletions