@menu
* Getting Started::
+* Pintos License::
* Pintos Trivia::
@end menu
Object file for the entire kernel. This is the result of linking
object files compiled from each individual kernel source file into a
single object file. It contains debug information, so you can run
-@command{gdb} or
+@command{gdb} or @command{backtrace} (@pxref{Backtraces}) on it.
@item kernel.bin
Memory image of the kernel. These are the exact bytes loaded into
but you can see a list of them using the @option{-u} option, e.g.@:
@code{pintos run -u}.
+@node Pintos License
+@section Pintos License
+
+Pintos is distributed under a liberal license that allows it to be
+freely used, modified, and distributed. Students and others own their
+own code and may use it for any purpose. In the context of Stanford's
+CS 140 course, please respect the spirit and the letter of the honor
+code by refraining from reading any homework solutions available
+online or elsewhere. (Source code for other operating system kernels,
+such as Linux or FreeBSD, is of course fair game.)
+
+There is NO WARRANTY for Pintos, not even for MERCHANTABILITY or
+FITNESS FOR A PARTICULAR PURPOSE.
+
+Please refer to the @file{LICENSE} file at the top level of the Pintos
+source distribution for details of license and lack of warranty.
+
@node Pintos Trivia
@section Pintos Trivia