Invent tid_t data type and use it in many places where we current use
[pintos-anon] / src /
drwxr-xr-x   ..
-rw-r--r-- 364 Makefile
-rw-r--r-- 3986 Makefile.build
-rw-r--r-- 275 Makefile.kernel
-rw-r--r-- 1295 TODO
-rw-r--r-- 342 constants.h
drwxr-xr-x - devices
drwxr-xr-x - filesys
drwxr-xr-x - lib
drwxr-xr-x - misc
drwxr-xr-x - threads
drwxr-xr-x - userprog
drwxr-xr-x - utils