From: Ben Pfaff <blp@cs.stanford.edu>
Date: Fri, 7 Nov 2008 05:19:34 +0000 (-0800)
Subject: Rename base_page_dir to init_page_dir.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;ds=sidebyside;h=fde3b8ee3eaf48b1a6bb14568aedc207e62accab;hp=fde3b8ee3eaf48b1a6bb14568aedc207e62accab;p=pintos-anon

Rename base_page_dir to init_page_dir.

This makes its name fit the convention that the file name is used as
a prefix for global symbol names.

Found by Godmar with his process-linker-map.pl script.
---