travis "failed to expand macro"

Stream: general

[Scott Morrison]

I just got another of these:

44.13s$ lean --recursive --export=mathlib.txt
<unknown>:1:1: error: failed to expand macro
The command "lean --recursive --export=mathlib.txt" exited with 1.

on travis.

[Scott Morrison]

https://travis-ci.org/leanprover/mathlib/jobs/454247679

[Scott Morrison]

lean --make . and lean --make . return happily.

[Reid Barton]

that's because you used sorry, I'm pretty sure

[Scott Morrison]

I remember someone else hitting this recently, but can't find it.

[Scott Morrison]

ah, okay, you're absolutely right, my mistake!