From b5f0874cd96ee2a62aabc645b9626c2749cb6a01 Mon Sep 17 00:00:00 2001
From: manuel <manuel@mausz.at>
Date: Mon, 26 Mar 2012 12:54:45 +0200
Subject: initial pintos checkin

---
 pintos-progos/utils/pintos-gdb | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100755 pintos-progos/utils/pintos-gdb

(limited to 'pintos-progos/utils/pintos-gdb')

diff --git a/pintos-progos/utils/pintos-gdb b/pintos-progos/utils/pintos-gdb
new file mode 100755
index 0000000..9c9555b
--- /dev/null
+++ b/pintos-progos/utils/pintos-gdb
@@ -0,0 +1,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
-- 
cgit v1.2.3