blob: 4ef38d3f177f1c9b694d422c14efdd2df98809d9 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
#! /bin/sh
# Path to GDB macros file. Customize for your site.
GDBMACROS=/usr/class/cs140/pintos/pintos/src/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
|
