Merging github pull request, occasionally accepted directly in github repository phpstorm/171.3039
authorDmitry Trofimov <dmitry.trofimov@jetbrains.com>
Tue, 7 Feb 2017 10:59:43 +0000 (13:59 +0300)
committerDmitry Trofimov <dmitry.trofimov@jetbrains.com>
Tue, 7 Feb 2017 10:59:43 +0000 (13:59 +0300)

Trivial merge