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

projects / pintos-anon / commit

summary | shortlog | log | commit | commitdiff | tree
(parent: 04b1db6) | 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	17102846d22591590c37548f8514067e2be6c5f6
tree	3b5accd9d4aca00ef312a6a15b4c5ed9161d51e3	tree \| snapshot
parent	04b1db625129936325474664d7f400b9993e9611	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