diff options
Diffstat (limited to 'stap-stop-server')
-rwxr-xr-x | stap-stop-server | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/stap-stop-server b/stap-stop-server new file mode 100755 index 00000000..5afcf705 --- /dev/null +++ b/stap-stop-server @@ -0,0 +1,30 @@ +#!/bin/bash + +# Start a systemtap server +# +# Copyright (C) 2008 Red Hat Inc. +# +# This file is part of systemtap, and is free software. You can +# redistribute it and/or modify it under the terms of the GNU General +# Public License (GPL); either version 2, or (at your option) any +# later version. + +# This script attempts to stop a systemtap server with the +# given pid. + +# Get the process id. +pid=$1 +if test "X$pid" = "X"; then + echo "Usage: $0 PROCESS_ID" >&2 + exit 1 +fi + +# Verify that it is a systemtap server +(ps -a | grep stap-serverd | grep -q $pid) +if test $? != 0; then + echo "$pid is not a systemtap server" + exit 1 +fi + +# Try to kill the server +kill -s SIGTERM $pid |