#! /bin/bash -

# Path to GDB macros file.  Customize for your site.
GDBMACROS=$(dirname $(which pintos))/gdb-macros

# Choose correct GDB.
if command -v i386-elf-gdb >/dev/null 2>&1; then
	GDB=i386-elf-gdb
else
	GDB=gdb
fi

if command -v mapsocket >/dev/null 2>&1; then
        GDB="mapsocket $GDB"
fi

# Run GDB.
if test -f "$GDBMACROS"; then
	exec $GDB -x "$GDBMACROS" "$@"
else
	echo "*** $GDBMACROS does not exist ***"
	echo "*** Pintos GDB macros will not be available ***"
	exec $GDB "$@"
fi