Re: make install; where do .di files go?

[David Nadlinger]

On Wednesday, 17 October 2012 at 23:08:32 UTC, Manu wrote:
Hear hear.

At least to me, it is not at all clear what you are trying to 
imply with this comment.

David