Fix some strange spacing apparently introduced by tools/indent.sh

This commit is contained in:
Gregory Nutt 2016-09-21 16:06:05 -06:00
parent 54eee5b303
commit d2e03daeb1