If you remove existing Pintos code, please delete it from your source
file entirely. Don't just put it into a comment or a conditional
compilation directive, because that makes the resulting code hard to
If you remove existing Pintos code, please delete it from your source
file entirely. Don't just put it into a comment or a conditional
compilation directive, because that makes the resulting code hard to