Closed jdahm closed 6 years ago
This is needed to fix a compilation error with GCC 8. As a side effect, my editor removed some extra whitespace at the end of a couple lines.
This is needed to fix a compilation error with GCC 8. As a side effect, my editor removed some extra whitespace at the end of a couple lines.