#!/bin/bash -x
ARGS="$*"
echo "Running arb_ntree in debugger (gdb)"
CMDS=ARB_debug.$$.commands
arb_echo "set args $ARGS" "source $ARBHOME/lib/BUGS/trace.gdb" > $CMDS
echo "---------- $CMDS"
cat $CMDS
echo "---------- execute in gdb"
gdb -n -batch -command=$CMDS arb_ntree
echo "---------- done"
rm $CMDS