scala-ide/scala-ide — pull request #715 by sschaef (2014-06-05 13:58:32+00:00)
Title: Pref update

This moves some Java preferences to the Scala editor, see the commit messages for more information.