pintos-os.org Git - pintos-anon/blob - src/utils/pintos-gdb

   1 #! /bin/sh
   2
   3 # Path to GDB macros file.  Customize for your site.
   4 GDBMACROS=/usr/class/cs140/pintos/pintos/src/misc/gdb-macros
   5
   6 # Choose correct GDB.
   7 if command -v i386-elf-gdb >/dev/null 2>&1; then
   8         GDB=i386-elf-gdb
   9 else
  10         GDB=gdb
  11 fi
  12
  13 # Run GDB.
  14 if test -f "$GDBMACROS"; then
  15         exec $GDB -x "$GDBMACROS" "$@"
  16 else
  17         echo "*** $GDBMACROS does not exist ***"
  18         echo "*** Pintos GDB macros will not be available ***"
  19         exec $GDB "$@"
  20 fi