On Wed, 13 Sep 2006 23:43:35 +0200, Denis Leroy wrote: > But yeah, probably not worth the effort. I don't see much wrong with > having /usr/include/CORE around either... Except that the name is very generic and hence short-sighted.