merging
authorChristian Grothoff <christian@grothoff.org>
Wed, 15 Mar 2017 10:34:58 +0000 (11:34 +0100)
committerChristian Grothoff <christian@grothoff.org>
Wed, 15 Mar 2017 10:34:58 +0000 (11:34 +0100)

Trivial merge