lampepfl/dotty — pull request #131 by odersky (2014-05-07 17:28:46+00:00)
Title: Fix/erasure

This is a pull request superseding fix/erasure2. I only added one more commit 12f2db0
but painted myself in a corner on which I could not back out. I pulled @DarkDimius last commit and then got into a state of git where I could neither revert nor commit my git state.

The good news is that I found what the problem is (even though I don't have enough git fu to fix it). It's in fact a problem I had for months. bin/dotc constantly gets messed up in my commits even though it is in my ./gitignore file. I now finally figured that bin/dotc is in fact a file in the commit tree. But in my Eclipse setup it is also the name of the dotc output directory! Can we please rename bin/dotc to some other file? bin is the std output directory in Eclipse and should therefore be ignored.