X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=src%2Futils%2Fpintos-gdb;h=4ef38d3f177f1c9b694d422c14efdd2df98809d9;hb=c809e9ba0a0dd653f20809d665ee7deb27aaac12;hp=c986b40a084cca196ffffe5080a9caf4b1603464;hpb=3bdc51472faafda1a37962cb2c7a00392f6a78bd;p=pintos-anon

diff --git a/src/utils/pintos-gdb b/src/utils/pintos-gdb
index c986b40..4ef38d3 100755
--- a/src/utils/pintos-gdb
+++ b/src/utils/pintos-gdb
@@ -11,7 +11,7 @@ else
 fi
 
 # Run GDB.
-if test -e "$GDBMACROS"; then
+if test -f "$GDBMACROS"; then
 	exec $GDB -x "$GDBMACROS" "$@"
 else
 	echo "*** $GDBMACROS does not exist ***"