diff options
| author |   Yann E. MORIN" <yann.morin.1998@anciens.enib.fr> | 2007-08-07 17:07:39 (GMT) |
|---|---|---|
| committer | Yann E. MORIN" <yann.morin.1998@anciens.enib.fr> | 2007-08-07 17:07:39 (GMT) |
| commit | f1741dc507fd560891cc3769385e72369b6cc7b8 (patch) | |
| tree | 8a716581e7a0de155d57269cff41030cb884d357 /tools | |
| parent | 3c0ae4744b85bf2f5c9d07896b025fdab1006365 (diff) | |
Fix the Makefile.in to correctly remove generated documentation.
Diffstat (limited to 'tools')
| -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 |