From f1741dc507fd560891cc3769385e72369b6cc7b8 Mon Sep 17 00:00:00 2001
From: "Yann E. MORIN\"" <yann.morin.1998@anciens.enib.fr>
Date: Tue, 7 Aug 2007 17:07:39 +0000
Subject: Fix the Makefile.in to correctly remove generated documentation.

---
 tools/populate.in | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/populate.in b/tools/populate.in
index 6d50fbe8..690dc5fb 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
-- 
cgit v1.2.3