Merge branch 'master' of git.bfh.ch:/staff/goc4/2018bti7061
authorChristian Grothoff <christian@grothoff.org>
Mon, 22 Oct 2018 15:27:44 +0000 (17:27 +0200)
committerChristian Grothoff <christian@grothoff.org>
Mon, 22 Oct 2018 15:27:44 +0000 (17:27 +0200)

Trivial merge