dealii/dealii — pull request #358 by tamiko (2014-12-18 09:16:58+00:00)
Title: Cherry-pick commits to the release branch

9e89d0b7a965e77afad6b50c7b7f77e399438337 (Wolfgang Bangerth)
Fix previous commit 1d327fd1dcd34023a3d5bb2c0ee7524593d44015.