From: Daniel Arndt Date: Wed, 15 Jan 2020 16:52:53 +0000 (-0700) Subject: Merge pull request #9333 from bangerth/pre X-Git-Tag: v9.2.0-rc1~672 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=77094b7b0a527271657b1c371642d0d95d649045;p=dealii.git Merge pull request #9333 from bangerth/pre Use @pre instead of @note in a number of places. --- 77094b7b0a527271657b1c371642d0d95d649045