/* getch, ungetch: buffered input with push-back. If too many characters are
   pushed back the program aborts. */

extern int getch(void);
extern void ungetch(int c);