Update name to Pintos.
[pintos-anon] / src /
drwxr-xr-x   ..
-rw-r--r-- 272 Makefile
-rw-r--r-- 3313 Makefile.build
-rw-r--r-- 275 Makefile.kernel
-rw-r--r-- 264 TODO
drwxr-xr-x - bochs
drwxr-xr-x - devices
drwxr-xr-x - filesys
drwxr-xr-x - lib
-rwxr-xr-x 625 pad
drwxr-xr-x - threads
drwxr-xr-x - userprog
drwxr-xr-x - vmware