#! /bin/sh DIR=`dirname $0` TOOL="" # start with valgrind if the first argument is --valgrind VALGRIND_OPTIONS="-v --tool=memcheck --leak-check=yes --show-reachable=no --leak-resolution=high --num-callers=40 --freelist-vol=4000000" if [ "$1" = "--valgrind" ] ; then echo "##### Running with Valgrind! ######" TOOL="valgrind $VALGRIND_OPTIONS" shift fi # start with gdb if the first argument is --gdb GDB_OPTIONS="-quiet -ex run" if [ "$1" = "--gdb" ] ; then echo "##### Running with GDB! ######" TOOL="gdb $GDB_OPTIONS --args" shift fi OPP_OPTIONS="-n $DIR:$DIR/../tutorials:$DIR/../showcases:$DIR/../examples --image-path=$DIR/../images $@" if [ -f $DIR/INET ]; then $TOOL $DIR/INET $OPP_OPTIONS elif [ -f $DIR/INET.exe ]; then $TOOL $DIR/INET.exe $OPP_OPTIONS else $TOOL opp_run -l $DIR/INET $OPP_OPTIONS fi