From: Wolfgang Bangerth Date: Thu, 28 Sep 2017 15:30:29 +0000 (-0600) Subject: Merge pull request #5106 from luca-heltai/extract-used-vertices X-Git-Tag: v9.0.0-rc1~1018 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=76900ac7d2fd9f24ee36a3ab43a902cc29bdbc7b;p=dealii.git Merge pull request #5106 from luca-heltai/extract-used-vertices GridTools::extract_used_vertices --- 76900ac7d2fd9f24ee36a3ab43a902cc29bdbc7b