X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fpintos.texi;h=40e702fc7831aa8ab5b1542b4a4e20413f5af474;hb=919347c164606c3f1544b2e8bd62f505aeda80a1;hp=ac1612717747f49d58407f8d581af178c931d1c0;hpb=392931f3f604f0c8ceb7d97dba21c7fefa2a2187;p=pintos-anon

diff --git a/doc/pintos.texi b/doc/pintos.texi
index ac16127..40e702f 100644
--- a/doc/pintos.texi
+++ b/doc/pintos.texi
@@ -1,4 +1,5 @@
 \input texinfo                          @c -*- texinfo -*-
+
 @c %**start of header
 @setfilename pintos.info
 @settitle Pintos Projects
@@ -66,6 +67,9 @@
 * License::
 @end menu
 
+@c institution-local settings
+@include localsettings.texi
+
 @include intro.texi
 @include threads.texi
 @include userprog.texi