merge
authorChristian Grothoff <christian@grothoff.org>
Tue, 1 May 2018 08:17:14 +0000 (10:17 +0200)
committerChristian Grothoff <christian@grothoff.org>
Tue, 1 May 2018 08:17:14 +0000 (10:17 +0200)

Trivial merge