Chris, > On 21 Nov 2018, at 10:12, Chris Jones <jon...@hep.phy.cam.ac.uk> wrote: > Do as you like, but I suspect /usr/include being missing is not a bug but > intentional.
I didn’t mean that. I mean the fact that when /usr/include exists, it is filled with outdated include files. Vincent
