Update license section.

diff --git a/doc/intro.texi b/doc/intro.texi
index 2897a3ab3ae9e5fa216f80f78715e95b0292c3f0..1c6584f4d9d0d4e8700f5a7651cf8b0ea56f1db8 100644 (file)
--- a/doc/intro.texi
+++ b/doc/intro.texi
@@ -253,12 +253,12 @@ 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.)
 
 online or elsewhere.  (Source code for other operating system kernels,
 such as Linux or FreeBSD, is of course fair game.)
 

-Please refer to the @file{LICENSE} file at the top level of the Pintos
-source distribution for license details.
-

 There is NO WARRANTY for Pintos, not even for MERCHANTABILITY or
 FITNESS FOR A PARTICULAR PURPOSE.
 
 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
 
 @node Pintos Trivia
 @section Pintos Trivia