Fix compilation error introduced in 6a39ed4.
Merge pull request #225 from bangerth/fix-previous-commit

Fix compilation error introduced in 6a39ed4.