Orc JIT vs. devtoolset-6

Thanks very much, David, that does the trick! We will make do with the special case and leave the general case as an exercise for the reader…