projects / pintos-anon / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (from: fde3b8e)
Rename base_page_dir to init_page_dir.
authorBen Pfaff <blp@cs.stanford.edu>
Fri, 7 Nov 2008 05:19:34 +0000 (21:19 -0800)
committerBen Pfaff <blp@cs.stanford.edu>
Fri, 7 Nov 2008 05:55:39 +0000 (21:55 -0800)
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.


No differences found
Pintos public repository