Fix the gdb configuration

f7d2b1a6 · Alexandru Dura · 9916dddc · f7d2b1a6
Commit f7d2b1a6 authored Mar 20, 2020 by Alexandru Dura
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

src/utils/pintos-gdb src/utils/pintos-gdb +1 -1

No files found.
--- a/src/utils/pintos-gdb
+++ b/src/utils/pintos-gdb
 #! /bin/sh

 # Path to GDB macros file.  Customize for your site.
-GDBMACROS=$HOME/pintos/src/misc/gdb-macros
+GDBMACROS=$PINTOS_HOME/src/misc/gdb-macros

 # Choose correct GDB.
 if command -v i386-elf-gdb >/dev/null 2>&1; then