tools/populate.in
changeset 316 e61d6151d807
parent 315 32cc893978ac
child 320 e585ed10bd5b
     1.1 --- a/tools/populate.in	Tue Aug 07 17:07:39 2007 +0000
     1.2 +++ b/tools/populate.in	Tue Aug 07 17:08:13 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 -    setsid nohup rm -rf "${CT_ROOT_DST_DIR}.$$" >/dev/null 2>&1 &
     1.8 +    nohup rm -rf "${CT_ROOT_DST_DIR}.$$" >/dev/null 2>&1 &
     1.9  fi
    1.10  
    1.11  # Create the working copy