I have just seen that /usr/ports/distfiles has grown up to 12 GiB. My hopefully not too stupid question is: Can I safely delete all files under /usr/ports/distfiles, e.g. # rm -rf /usr/ports/distfiles/* I strongly suppose so but I am not sure. Thanks for any feedback. Regards, Peter