Re: can't get desired font in one user's terminal. [SOLVED]