diff options
author | Martin Odersky <odersky@gmail.com> | 2013-08-10 12:32:04 +0200 |
---|---|---|
committer | Martin Odersky <odersky@gmail.com> | 2013-08-10 12:32:04 +0200 |
commit | 4b32ec471bafe988b64563aaabf2d273220a8644 (patch) | |
tree | f9a1530385e8fc9e0d1ded6b1c755f140fd3b64e /.gitattributes | |
parent | d318cafbb92518a39c84539c0387c2c93815bb7a (diff) | |
download | dotty-4b32ec471bafe988b64563aaabf2d273220a8644.tar.gz dotty-4b32ec471bafe988b64563aaabf2d273220a8644.tar.bz2 dotty-4b32ec471bafe988b64563aaabf2d273220a8644.zip |
Added typing of Alternatives.
Also changed some maps to mapconserves to avoid unnecessary tree copying.
Diffstat (limited to '.gitattributes')
0 files changed, 0 insertions, 0 deletions