Ignore pintos.text.
[pintos-anon] / src / devices /
drwxr-xr-x   ..
-rw-r--r-- 16103 disk.c
-rw-r--r-- 670 disk.h
-rw-r--r-- 2826 intq.c
-rw-r--r-- 1416 intq.h
-rw-r--r-- 5714 kbd.c
-rw-r--r-- 170 kbd.h
-rw-r--r-- 5175 serial.c
-rw-r--r-- 218 serial.h
-rw-r--r-- 4996 timer.c
-rw-r--r-- 495 timer.h
-rw-r--r-- 2805 vga.c
-rw-r--r-- 116 vga.h