Just to follow up on this, many moons later: The fix for this problem turns out to be only one line long. That didn't make it easier to find, though :-) It can be found at https://github.com/dealii/dealii/pull/3589 and should become part of the next release.
Best Wolfgang -- The deal.II project is located at http://www.dealii.org/ For mailing list/forum options, see https://groups.google.com/d/forum/dealii?hl=en --- You received this message because you are subscribed to the Google Groups "deal.II User Group" group. To unsubscribe from this group and stop receiving emails from it, send an email to dealii+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
