Fixed spelling of tilde
commitf801dfc5665f8d512c8d473313c7b41b8171310f
authorJan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk>
dateTue 1 Aug 2017, 08:39 (9 years ago)
parentf2c4091
libs/contrib/Text/PrettyPrint/WL/Characters.idr+2−2
@@ -69,8 +69,8 @@ bang = char '!'
6969tick : Doc
7070tick = char '`'
7171
72−tilda : Doc
73−tilda = char '~'
72+tilde : Doc
73+tilde = char '~'
7474
7575hash : Doc
7676hash = char '#'