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=4ef38d3f177f1c9b694d422c14efdd2df98809d9;hb=2de6c3a98848de085ca065b42b4e3df9741345ac;hp=c986b40a084cca196ffffe5080a9caf4b1603464;hpb=82281a670902d91868eb968db65a8c0dc9b4e502;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 ***"