Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Correct a typo which might have lead to a dump.
Noted by Martin Kraemer <Martin.Kraemer@Fujitsu-Siemens.com>
- Loading branch information