dealii/dealii — pull request #250 by bangerth (2014-11-13 21:13:54+00:00)
Title: Fix the previous commit so that it doesn't produce a warning.

I botched the previous pull request in my hurry to get it out. It worked, but only with a warning. This one does it right.