diff --git a/kernel_dev.c b/kernel_dev.c
index 9e27bfc..5a9c749 100644
--- a/kernel_dev.c
+++ b/kernel_dev.c
@@ -1,5 +1,7 @@
 
 #include <assert.h>
+#include <stdlib.h>
+
 #include "kernel_cc.h"
 #include "kernel_dev.h"
 #include "kernel_sched.h"
@@ -184,6 +186,85 @@ file_ops serial_fops = {
 };
 
 
+/*============================================
+
+  The terminal device driver
+
+ ============================================*/
+
+typedef struct terminal_device_stream {
+  void* serial_stream;
+  file_ops* serial_ops;
+  int pending_eof;
+} terminal_stream_t;
+
+static void* terminal_open(uint term)
+{
+  terminal_stream_t* stream = xmalloc(sizeof(*stream));
+  stream->serial_stream = serial_open(term);
+  stream->serial_ops = &serial_fops;
+  stream->pending_eof = 0;
+  return stream;
+}
+
+static int terminal_read(void* dev, char *buf, unsigned int size)
+{
+  terminal_stream_t* stream = (terminal_stream_t*)dev;
+
+  if(stream->pending_eof) {
+    stream->pending_eof = 0;
+    return 0;
+  }
+
+  unsigned int count = 0;
+  while(count < size) {
+    char ch;
+    int rc = stream->serial_ops->Read(stream->serial_stream, &ch, 1);
+
+    if(rc < 0)
+      return rc;
+
+    if(rc == 0) {
+      if(count == 0)
+        return 0;
+      break;
+    }
+
+    if(ch == 4) {
+      if(count == 0) {
+        return 0;
+      }
+      stream->pending_eof = 1;
+      break;
+    }
+
+    buf[count++] = ch;
+  }
+
+  return count;
+}
+
+static int terminal_write(void* dev, const char* buf, unsigned int size)
+{
+  terminal_stream_t* stream = (terminal_stream_t*)dev;
+  return stream->serial_ops->Write(stream->serial_stream, buf, size);
+}
+
+static int terminal_close(void* dev)
+{
+  terminal_stream_t* stream = (terminal_stream_t*)dev;
+  stream->serial_ops->Close(stream->serial_stream);
+  free(stream);
+  return 0;
+}
+
+static file_ops terminal_fops = {
+  .Open = terminal_open,
+  .Read = terminal_read,
+  .Write = terminal_write,
+  .Close = terminal_close
+};
+
 
 /***********************************
 
@@ -206,6 +287,10 @@ void initialize_devices()
   devtable[DEV_SERIAL].devnum = bios_serial_ports();
   devtable[DEV_SERIAL].dev_fops = serial_fops;
 
+  devtable[DEV_TERMINAL].type = DEV_TERMINAL;
+  devtable[DEV_TERMINAL].devnum = bios_serial_ports();
+  devtable[DEV_TERMINAL].dev_fops = terminal_fops;
+
   /* Initialize the serial devices */
   for(int i=0; i<bios_serial_ports(); i++) {
     serial_dcb[i].devno = i;
diff --git a/kernel_dev.h b/kernel_dev.h
index bbe333a..e0beb46 100644
--- a/kernel_dev.h
+++ b/kernel_dev.h
@@ -23,7 +23,7 @@
   The Major number determines the driver routines related to
   the device. The Minor number is used to specify one among
   several devices of the same Major number. For example,
-  device (DEV_SERIAL,2) is the 3rd serial terminal.
+  device (DEV_TERMINAL,2) is the 3rd terminal.
 
   The device table lists the devices by major number, and gives
   the number of devices for this type. It also contains 
@@ -102,9 +102,10 @@ typedef struct file_operations {
   The device type of a device determines the driver used.
 */
 typedef enum { 
-	DEV_NULL,    /**< @brief Null device */
-	DEV_SERIAL,  /**< @brief Serial device */
-	DEV_MAX      /**< @brief placeholder for maximum device number */
+        DEV_NULL,      /**< @brief Null device */
+        DEV_SERIAL,    /**< @brief Serial device */
+        DEV_TERMINAL,  /**< @brief Terminal device */
+        DEV_MAX        /**< @brief placeholder for maximum device number */
 }  Device_type;
 
 
diff --git a/kernel_streams.c b/kernel_streams.c
index d6d0e0d..23cd24d 100644
--- a/kernel_streams.c
+++ b/kernel_streams.c
@@ -241,7 +241,7 @@ int sys_Dup2(int oldfd, int newfd)
 
 unsigned int sys_GetTerminalDevices()
 {
-  return device_no(DEV_SERIAL);
+  return device_no(DEV_TERMINAL);
 }
 
 
@@ -278,6 +278,6 @@ int sys_OpenNull()
 
 Fid_t sys_OpenTerminal(unsigned int termno)
 {
-  return open_stream(DEV_SERIAL, termno);
+  return open_stream(DEV_TERMINAL, termno);
 }
 
diff --git a/tinyos.h b/tinyos.h
index 2bdf43b..560b9f6 100644
--- a/tinyos.h
+++ b/tinyos.h
@@ -392,10 +392,13 @@ unsigned int GetTerminalDevices();
 
   @param termno the terminal number to open
   @return the file ID of the new descriptor
-    On success, OpenTerminal returns the file id for a new file for this 
+    On success, OpenTerminal returns the file id for a new file for this
    terminal. On error, it returns @c NOFILE. Possible errors are:
    - The terminal device does not exist.
    - The maximum number of file descriptors has been reached.
+
+   The terminal device translates the @c ^D character (ASCII 4) into an end of
+   stream indication, matching standard Unix terminal behaviour.
  */
 Fid_t OpenTerminal(unsigned int termno);
 
diff --git a/tinyos_shell.c b/tinyos_shell.c
index c04f639..b5e9096 100644
--- a/tinyos_shell.c
+++ b/tinyos_shell.c
@@ -167,7 +167,7 @@ int RunTerm(size_t argc, const char** argv)
 int SystemInfo(size_t argc, const char** argv)
 {
 	printf("Number of cores         = %d\n", cpu_cores());
-	printf("Number of serial devices= %d\n", bios_serial_ports());
+        printf("Number of terminal devices= %d\n", GetTerminalDevices());
 	Fid_t finfo = OpenInfo();
 	if(finfo!=NOFILE) {
 		/* Print per-process info */