From: Bruno Turcksin Date: Thu, 3 Nov 2016 14:18:37 +0000 (-0400) Subject: Merge pull request #3428 from bangerth/remove-accidental-files X-Git-Tag: v8.5.0-rc1~497 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=a44654ea03e66f1fbd2d266d3e23afd5084e52d4;p=dealii.git Merge pull request #3428 from bangerth/remove-accidental-files Remove accidentally added files. --- a44654ea03e66f1fbd2d266d3e23afd5084e52d4