[Agda-dev] Why do we support cpp?

[Jesper Cockx]

Hi all,

Maybe I'm beating a dead horse here, but why do we still also support cpp
instead of only cpphs if cpp can't even properly handle primes (')? This is
extremely annoying and hits me in >50% of the cases when I push something.
I know about the issue where 'build-depends' in the cabal file doesn't
automatically install the dependencies, but couldn't we just add 'cabal
install cpphs' to the makefile and drop support for cpp? This seems like a
much better solution than polluting our code with {-'-} or additional line
breaks.

-- Jesper

ps: sorry for the rant.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20180518/ffa92b0c/attachment.html>