3 # Path to GDB macros file. Customize for your site.
4 GDBMACROS=/usr/class/cs140/pintos/pintos/src/misc/gdb-macros
7 if command -v i386-elf-gdb >/dev/null 2>&1; then
14 if test -e "$GDBMACROS"; then
15 exec $GDB -x "$GDBMACROS" "$@"
17 echo "*** $GDBMACROS does not exist ***"
18 echo "*** Pintos GDB macros will not be available ***"