diff options
| -rwxr-xr-x[-rw-r--r--] | src/utils/pintos-gdb | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/utils/pintos-gdb b/src/utils/pintos-gdb index 4ef38d3..f5679d4 100644..100755 --- a/src/utils/pintos-gdb +++ b/src/utils/pintos-gdb @@ -1,7 +1,7 @@ -#! /bin/sh +#! /bin/bash - # Path to GDB macros file. Customize for your site. -GDBMACROS=/usr/class/cs140/pintos/pintos/src/misc/gdb-macros +GDBMACROS=$(dirname $(which pintos))/gdb-macros # Choose correct GDB. if command -v i386-elf-gdb >/dev/null 2>&1; then @@ -10,6 +10,10 @@ else GDB=gdb fi +if command -v mapsocket >/dev/null 2>&1; then + GDB="mapsocket $GDB" +fi + # Run GDB. if test -f "$GDBMACROS"; then exec $GDB -x "$GDBMACROS" "$@" |