20 lines
413 B
Bash
Executable file
20 lines
413 B
Bash
Executable file
#! /bin/sh
|
|
|
|
# Path to GDB macros file. Customize for your site.
|
|
GDBMACROS=/pintos-env/pintos/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
|