From: David Wells <drwells@email.unc.edu>
Date: Sat, 18 May 2019 17:33:30 +0000 (-0400)
Subject: Merge pull request #8239 from bangerth/update
X-Git-Tag: v9.2.0-rc1~1469
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=b2c06f1827d2cd0254f1de6fe7c3a8038ec95087;p=dealii.git

Merge pull request #8239 from bangerth/update

Update a comment in the doxygen options file.
---

b2c06f1827d2cd0254f1de6fe7c3a8038ec95087