+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
+read. We're only going to do a compile in the directory for the current
+project, so you don't need to make sure that the previous projects also
+compile.
+