-The second command loads the 16bit symbols a second time at an offset
-of 0xf0000, which helps gdb set and catch breakpoints correctly.
-
-To debug a VGA BIOS image, run "gdb out/vgarom.o" add use the gdb
-command "add-symbol-file out/vgarom.o 0xc0000" to load the 16bit VGA
+To debug a VGA BIOS image, run `gdb out/vgarom.o`, create a
+vgaromoffset.o file with offset 0xc0000, add use the gdb
+command `add-symbol-file out/vgaromoffset.o 0` to load the 16bit VGA