diff -r e61d6151d807 -r e585ed10bd5b tools/populate.in
--- a/tools/populate.in	Tue Aug 07 17:08:13 2007 +0000
+++ b/tools/populate.in	Tue Aug 07 18:05:41 2007 +0000
@@ -71,7 +71,7 @@
 # Get rid of potentially older destination directory
 if [ -d "${CT_ROOT_DST_DIR}" ]; then
     mv "${CT_ROOT_DST_DIR}" "${CT_ROOT_DST_DIR}.$$"
-    nohup rm -rf "${CT_ROOT_DST_DIR}.$$" >/dev/null 2>&1 &
+    setsid nohup rm -rf "${CT_ROOT_DST_DIR}.$$" >/dev/null 2>&1 &
 fi
 
 # Create the working copy