From: John Ousterhout <ouster@cs.stanford.edu>
Date: Wed, 28 Mar 2018 16:59:11 +0000 (-0700)
Subject: Fix problems compiling documentation
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=c3f2bdb4fcd99dca631962dccb21214e2847f3a3;hp=c3f2bdb4fcd99dca631962dccb21214e2847f3a3;p=pintos-anon

Fix problems compiling documentation
* Two warnings (deprecated regex syntax)
* One error (couldn't find pintos-t2h.init without "./" prefix)
---