Update settings/tools menu name#12

Merged

ThomasKranitsas merged 4 commits intotopcoder-platform:developfrom

nauhil:develop

Jun 26, 2018

Commits on Jun 25, 2018

Update settings/tools menu name
Huan Li
committed

Commits on Jun 26, 2018