1 files changed, 0 insertions, 21 deletions

diff --git a/pintos-progos/utils/pintos-gdb b/pintos-progos/utils/pintos-gdb
deleted file mode 100755
index 9c9555b..0000000
--- a/pintos-progos/utils/pintos-gdb
+++ /dev/null
@@ -1,21 +0,0 @@
-#! /bin/sh
-
-# Path to GDB macros file.  Customize for your site.
-PINTOS_SRC="$(dirname $(dirname $(which pintos-gdb)))"
-GDBMACROS="${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 -f "$GDBMACROS"; then
-        exec $GDB -x "$GDBMACROS" "$@"
-else
-        echo "*** $GDBMACROS does not exist ***"
-        echo "*** Pintos GDB macros will not be available ***"
-        exec $GDB "$@"
-fi