Tools: generate a core file for a given PID

Similarly to dumpstack.sh, uses gdb to dump a core file

Tools/scripts/dumpcore.sh

@@ -0,0 +1,17 @@
+#!/bin/sh
+
+# attaches GDB to a process to dump a core
+
+# we want everything on stderr, so the program is not disturbed
+exec 1>&2
+
+PID=$1
+TMPFILE=/tmp/gdb.$$
+COREFILE="ap-$$.core"
+cat << EOF  > $TMPFILE
+set height 0
+generate-core-file $COREFILE
+quit
+EOF
+gdb -n -batch -x $TMPFILE --pid $PID < /dev/null 2>&1
+/bin/rm -f $TMPFILE