Always try to create output directory, even if pintos directory exists.
-rw-r--r-- 1341 AUTHORS
-rw-r--r-- 4270 LICENSE
drwxr-xr-x - doc
drwxr-xr-x - grading
drwxr-xr-x - specs
drwxr-xr-x - src