Ed Schouten 790dd1b5af Just use ttydisc_rint_simple() instead of doing it ourselves.
This code seems to do exactly the same as ttydisc_rint_simple() does
nowadays. Just remove it.

Obtained from:	//depot/user/ed/newcons/sys/dev/syscons/syscons.c
2009-09-18 15:39:09 +00:00
..