From: Wolfgang Bangerth Date: Mon, 19 Jun 2017 05:15:11 +0000 (-0600) Subject: Merge pull request #4519 from luca-heltai/key-value-separator-in-map-pattern X-Git-Tag: v9.0.0-rc1~1493 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=b22c6430c9e5cbb9db3f9e09ec9123e0355eba91;p=dealii.git Merge pull request #4519 from luca-heltai/key-value-separator-in-map-pattern Key Value separator in Patterns::Map --- b22c6430c9e5cbb9db3f9e09ec9123e0355eba91