From: David Wells <drwells@email.unc.edu>
Date: Fri, 27 Jan 2023 22:29:04 +0000 (-0500)
Subject: Merge pull request #14741 from bangerth/index-set
X-Git-Tag: v9.5.0-rc1~592
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=d77e5ebb0af4487fa3c503f97fd9d126f2eac18f;p=dealii.git

Merge pull request #14741 from bangerth/index-set

Introduce IndexSet::get_index_vector().
---

d77e5ebb0af4487fa3c503f97fd9d126f2eac18f