(no commit message)

diff --git a/contrib/timeout_watchdog.c b/contrib/timeout_watchdog.c
index b31c4e6cfa1cd48bff06fafe9dbe44254a721847..d257d04de73aa6e53337bcd0607dddb32559a56d 100644 (file)
--- a/contrib/timeout_watchdog.c
+++ b/contrib/timeout_watchdog.c
@@ -98,7 +98,7 @@ if (child > 0)
 {
   sleep(timeout);
   printf("Child processes were killed after timeout of %u seconds\n",timeout);
-  kill(0,SIGABRT);
+  kill(0,SIGTERM);
   exit(1);
 }  
 exit(1);