blob: 9c9555bb27a576b748fdb667084e85565b90612f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
#! /bin/sh
# Path to GDB macros file. Customize for your site.
PINTOS_SRC="$(dirname $(dirname $(which pintos-gdb)))"
GDBMACROS="${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
|
