Build #420 (03.08.2017 19:36:30)

1. merge in new documentation (commit: 71506e7) (detail / githubweb)

Started by remote host 192.30.252.34 with note: null

• refs/remotes/origin/master