From: Wolfgang Bangerth Date: Sat, 9 Apr 2016 12:37:48 +0000 (-0500) Subject: Merge pull request #2492 from luca-heltai/hot-fix X-Git-Tag: v8.5.0-rc1~1120 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=be60606fdc3c53ec91c134a4a62c2ff4ad35af66;p=dealii.git Merge pull request #2492 from luca-heltai/hot-fix Restore a line removed by accident. --- be60606fdc3c53ec91c134a4a62c2ff4ad35af66