--- /dev/null
+#! /bin/sh
+
+# Path to GDB macros file. Customize for your site.
+GDBMACROS=/usr/class/cs140/pintos/pintos/src/misc/gdb-macros
+
+# Choose correct GDB.
+if command -v i386-elf-gdb >/dev/null 2>&1; then
+ GDB=i386-elf-gdb
+else
+ GDB=gdb
+fi
+
+# Run GDB.
+if test -e "$GDBMACROS"; then
+ exec $GDB -x "$GDBMACROS" "$@"
+else
+ echo "*** $GDBMACROS does not exist ***"
+ echo "*** Pintos GDB macros will not be available ***"
+ exec $GDB "$@"
+fi