On 2017-11-16 14:03, Axel Dörfler wrote:
Am 16/11/2017 um 15:48 schrieb kallisti5:
I guess this is what needs to happen?
https://gist.github.com/kallisti5/762cb0eac31986962d725484f79a1e04
We don't put our names into public headers; they are just defining a
public API, they don't express your own choices :-)