This repository has been archived on 2021-05-26. You can view files and clone it, but cannot push or open issues or pull requests.
OS/pintos-env/pintos/utils/pintos-gdb

21 lines
413 B
Text
Raw Normal View History

#! /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