pintos-os.org Git - pintos-anon/commit

projects / pintos-anon / commit

summary | shortlog | log | commit | commitdiff | tree
(parent: 0122bc0) | patch

author	Godmar Back <godmar@gmail.com>
	Wed, 13 Sep 2006 11:40:40 +0000 (11:40 +0000)
committer	Godmar Back <godmar@gmail.com>
	Wed, 13 Sep 2006 11:40:40 +0000 (11:40 +0000)
commit	3b6ef3f86bdb454cca9a5ce62c1845f019dba46a
tree	8bf7d9e9d13740df06550ca7083b2d9a4529841f	tree \| snapshot
parent	0122bc0324000ff7b497d1ddce881aa4e702b34b	commit \| diff

fixed left-over, now-wrong comment about how decrease in numeric priority means increase in effective priority

diff | blob | history

Pintos public repository