[Agda-dev] COMPILE pragma not allowed in safe mode.

[John Leo]

Hi everyone,

I just pulled the latest agda and agda-stdlib and while agda builds fine I
get a bunch of errors in the stdlib code (for example in Data/Empty.agda):
COMPILE pragma not allowed in safe mode.

I don't know if this is a new check that was added and the stdlib has just
not been updated yet but I thought I'd point it out. If you like I can file
a bug. I've just commented out the offending COMPILE statements in my own
code for now.

John
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.chalmers.se/mailman/private/agda-dev/attachments/20190201/a4af6c38/attachment.html>