From: Timo Heister Date: Mon, 8 Sep 2014 01:35:42 +0000 (-0400) Subject: Merge pull request #138 from bangerth/delete-outdated-file X-Git-Tag: v8.2.0-rc1~156 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=ad89c4a4ece0dd575c1a262555fa4b739867ecfd;p=dealii.git Merge pull request #138 from bangerth/delete-outdated-file Remove a file that was probably never intended to be added. --- ad89c4a4ece0dd575c1a262555fa4b739867ecfd