What On Aug 20, 2013 6:14 AM, "John Cremona" <[email protected]> wrote: > > 5.12 introduced a new encoding for the Sage header. I remember some > discussion on this list of whether it was a good idea or not. I > probably cannot cut and paste here to show you how weird this looks > for me, but it's a mess of chinese-looking characters: > > ┌────────────────────────────────────────────────────────────────────┠> │ Sage Version 5.12.beta1, Release Date: 2013-08-16 │ > │ Type "notebook()" for the browser-based notebook interface. │ > │ Type "help()" for help. │ > └────────────────────────────────────────────────────────────────────┘ > ┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┓ > ┃ Warning: this is a prerelease version, and it may be unstable. ┃ > ┗┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┠┛ > sage: > > (they are not all a-circumflex as tey appear in my gmail window). > > I tried switching my locale setting but it made no difference. What > magic do I need to use to make this look reasonable? And then we > should add instructions to the FAQ since we'll surely get many more > similar comments? (I confess that I did not check the FAQ before > posting this....)
What terminal are you using? Rxvt, xterm, konsole, ? > > John > > -- > You received this message because you are subscribed to the Google Groups "sage-devel" group. > To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. > To post to this group, send email to [email protected]. > Visit this group at http://groups.google.com/group/sage-devel. > For more options, visit https://groups.google.com/groups/opt_out. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/groups/opt_out.
