diff options
author | Yann E. MORIN" <yann.morin.1998@anciens.enib.fr> | 2007-08-07 18:05:41 (GMT) |
---|---|---|
committer | Yann E. MORIN" <yann.morin.1998@anciens.enib.fr> | 2007-08-07 18:05:41 (GMT) |
commit | feb0328d7a519eb63999fdbc450cd706bec8df51 (patch) | |
tree | 45fb279fc532b06dde1a8f2487fc79672d52ac03 /tools/populate.in | |
parent | a43770ab06261620debcfe1a9bab28babf5ec37f (diff) |
Make use of setsid to spawn removal processes: we don't want the rm's to stop if the main script fails and ends before all directories were removed.
Diffstat (limited to 'tools/populate.in')
-rw-r--r-- | tools/populate.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/populate.in b/tools/populate.in index 6d50fbe..690dc5f 100644 --- a/tools/populate.in +++ b/tools/populate.in @@ -71,7 +71,7 @@ fi # 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 |