Commit dfe5d3e4 authored Apr 30, 2019 by Andreas Klöckner

Merge branch 'gh' into 'master'

Merge github master

See merge request inducer/pyopencl!82