devices_SRC += devices/vga.c # Video device.
devices_SRC += devices/serial.c # Serial port device.
devices_SRC += devices/disk.c # IDE disk device.
devices_SRC += devices/vga.c # Video device.
devices_SRC += devices/serial.c # Serial port device.
devices_SRC += devices/disk.c # IDE disk device.
devices_SRC += devices/intq.c # Interrupt queue.
# Library code shared between kernel and user programs.
devices_SRC += devices/intq.c # Interrupt queue.
# Library code shared between kernel and user programs.