idris-lang/Idris-dev — pull request #1314 by WithHat (2014-06-13 16:00:42+00:00)
Title: Removed Unicode character from source file

Unicode is discouraged according to https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291