-extracting it into a directory. Then read
-@file{pintos/src/misc/bochs-2.2.6.README} and apply the patches needed.
-Then run @file{./configure}, supplying the options you want (some
-suggestions are in the patch file). Finally, run @command{make}.
-This will compile Bochs and eventually produce a new binary
-@file{bochs}. To use your @file{bochs} binary with @command{pintos},
+saving the file @file{bochs-2.2.6.tar.gz} into a directory.
+The script @file{pintos/src/misc/bochs-2.2.6-build.sh}
+applies a number of patches contained in @file{pintos/src/misc}
+to the Bochs tree, then builds Bochs and installs it in a directory
+of your choice.
+Run this script without arguments to learn usage instructions.
+To use your @file{bochs} binary with @command{pintos},