GPL build fix mistakenly merged into master This reverts commit fd862e9828d544f593a622f2914d1257366ae802.