From: John Darrington <john@darrington.wattle.id.au>
Date: Wed, 3 Jul 2019 18:01:30 +0000 (+0200)
Subject: Remove UNUSED attributes where they were inappropriate.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=7a09f7e0127967c4f04a51f1b9cf91040c515c34;hp=7a09f7e0127967c4f04a51f1b9cf91040c515c34;p=pspp

Remove UNUSED attributes where they were inappropriate.

These parameters were marked UNUSED, when they were in fact,
used.
---