blob: f5679d4723592ebf686c576d0bd4117ce59ef780 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
#! /bin/bash -
# Path to GDB macros file. Customize for your site.
GDBMACROS=$(dirname $(which pintos))/gdb-macros
# Choose correct GDB.
if command -v i386-elf-gdb >/dev/null 2>&1; then
GDB=i386-elf-gdb
else
GDB=gdb
fi
if command -v mapsocket >/dev/null 2>&1; then
GDB="mapsocket $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
|
