Fix naming and availability in command palette of various commands#377
Merged
jcreedcmu merged 4 commits intogithub:masterfrom May 19, 2020
Merged
Fix naming and availability in command palette of various commands#377jcreedcmu merged 4 commits intogithub:masterfrom
jcreedcmu merged 4 commits intogithub:masterfrom