X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Futils%2Fpintos-gdb;fp=src%2Futils%2Fpintos-gdb;h=c986b40a084cca196ffffe5080a9caf4b1603464;hb=51d220e8f5774ddb62aee7a266a79e5c12e605e4;hp=0000000000000000000000000000000000000000;hpb=bfd2e965e1aa5f2b00dff6b11be770c6cbe7313d;p=pintos-anon

diff --git a/src/utils/pintos-gdb b/src/utils/pintos-gdb
new file mode 100755
index 0000000..c986b40
--- /dev/null
+++ b/src/utils/pintos-gdb
@@ -0,0 +1,20 @@
+#! /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