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)
commitb7869370b8b58bf191c0cb448ced60f7f20508db
tree142c0b3bf714d8cde69ad6d5fd1fbfdbfd6e9394
parent8e9039e6268fe47556dcf393a4c25c113f909178
parent02360d573d0ff46b34ea0d94321e46688959e477
Merge branch 'master' of git.bfh.ch:/staff/goc4/2018bti7061