Merge branch 'master' of git.bfh.ch:/staff/goc4/2018bti7061
authorChristian Grothoff <christian@grothoff.org>
Tue, 25 Sep 2018 18:09:49 +0000 (20:09 +0200)
committerChristian Grothoff <christian@grothoff.org>
Tue, 25 Sep 2018 18:09:49 +0000 (20:09 +0200)

Trivial merge