Clean up temp files on signal.

diff --git a/src/utils/pintos b/src/utils/pintos
index afd0ec280f356516bd29e8db098d66649cb7df01..f99396841aa65f3873a8cf11145637ae1d7ff489 100755 (executable)
--- a/src/utils/pintos
+++ b/src/utils/pintos
@@ -677,10 +677,11 @@ sub xsystem {
 # relay_signal($pid, $signal)
 #
 # Relays $signal to $pid and then reinvokes it for us with the default
-# handler.
+# handler.  Also cleans up temporary files.
 sub relay_signal {
     my ($pid, $signal) = @_;
     kill $signal, $pid;
+    File::Temp::cleanup();
     $SIG{$signal} = 'DEFAULT';
     kill $signal, getpid ();
 }