add comments for fancy unicode
Closed this issue · 2 comments
when you define a datatype that uses some fancy rare unicode character, it'd be useful for there to be a comment saying how to enter it using the standard emacs agda thing
This is exactly keys.md. It's slightly but not very much out of date
because I prioritized other things during the run up to the deadline.
---Ian
On Jul 7, 2016 11:31 PM, "Cyrus Omar" notifications@github.com wrote:
when you define a datatype that uses some fancy rare unicode character,
it'd be useful for there to be a comment saying how to enter it using the
standard emacs agda thing—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#20, or mute the thread
https://github.com/notifications/unsubscribe/AD6MIJczFF5QlC779DvG8l55VP5RBHf-ks5qTcShgaJpZM4JHsdt
.
Ah OK, didn't notice that. Maybe highlight it in the README too.
On Fri, Jul 8, 2016 at 1:45 PM Ian Voysey notifications@github.com wrote:
This is exactly
keys.md. It's slightly but not very much out of date
because I prioritized other things during the run up to the deadline.---Ian
On Jul 7, 2016 11:31 PM, "Cyrus Omar" notifications@github.com wrote:when you define a datatype that uses some fancy rare unicode character,
it'd be useful for there to be a comment saying how to enter it using the
standard emacs agda thing—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#20, or mute the
thread
<
https://github.com/notifications/unsubscribe/AD6MIJczFF5QlC779DvG8l55VP5RBHf-ks5qTcShgaJpZM4JHsdt.
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
#20 (comment),
or mute the thread
https://github.com/notifications/unsubscribe/AARIPmSqunIwxAx6ik0_gbodQ46t02s7ks5qTozCgaJpZM4JHsdt
.