They probably didn't even know that their work had filled /tmp so
thanks for making this known.
To make this less likely to happen in future (or, at least, be
self-repairing!) an admin could add
find /tmp -type f -mtime +1 -exec rm {} \;
find /tmp/* -type d -empty -exec rmdir {} \;
in a cron job.
Cheers
M