More thorough cleaning of /tmp on jenkins.

diff --git a/tools/jenkins/build.sh b/tools/jenkins/build.sh
index ae085a7..3a84ab2 100755 (executable)
--- a/tools/jenkins/build.sh
+++ b/tools/jenkins/build.sh
@@ -9,6 +9,8 @@
 export LC_ALL=C
 
 echo "XXXX Cleanup previous attempts. Remaining content of /tmp:"
+rm -f /tmp/cc*
+rm -f /tmp/*.so
 rm -rf /tmp/simgrid-java*
 rm -rf /var/tmp/simgrid-java*
 rm -rf /tmp/jvm-*