diff -r 3abd6e8a0067 -r 32cc893978ac tools/populate.in --- a/tools/populate.in Sat Jul 14 21:21:55 2007 +0000 +++ b/tools/populate.in Tue Aug 07 17:07:39 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