Merge pull request #4976 from anhu/kill_tabs

Get rid of tabs I added previously.
This commit is contained in:
David Garske
2022-03-22 11:35:00 -07:00
committed by GitHub