changeset 345 | 4d618b3b3de5 |
parent 316 | e61d6151d807 |
child 523 | 010f6f4e4dd6 |
1.1 --- a/tools/populate.in Tue Aug 07 17:08:13 2007 +0000 1.2 +++ b/tools/populate.in Wed Aug 29 16:46:23 2007 +0000 1.3 @@ -71,7 +71,7 @@ 1.4 # Get rid of potentially older destination directory 1.5 if [ -d "${CT_ROOT_DST_DIR}" ]; then 1.6 mv "${CT_ROOT_DST_DIR}" "${CT_ROOT_DST_DIR}.$$" 1.7 - nohup rm -rf "${CT_ROOT_DST_DIR}.$$" >/dev/null 2>&1 & 1.8 + setsid nohup rm -rf "${CT_ROOT_DST_DIR}.$$" >/dev/null 2>&1 & 1.9 fi 1.10 1.11 # Create the working copy