Fix typo

[pchaigno]

No description provided.

[pchaigno]

@soonhokong Did you get a chance to look into this?

[soonho-tri]

@pchaigno , I'm not sure that pattern is a typo of patterns given https://github.com/leanprover/lean/search?l=Lean&q=pattern&type=&utf8=%E2%9C%93.

[pchaigno]

pattern is the key in the Sublime Text grammar format here, not a Lean keyword.

[soonho-tri]

Ah, I see. Sounds good to me then. @leodemoura , could you merge this PR?

[leodemoura]

@soonho-tri Thanks for looking into this stuff.

@pchaigno I will merge this PR later (not in the next few weeks). I am currently busy, and I don't like to merge PRs without testing them.

[pchaigno]

@leodemoura Did you get a chance to test this pull request?

[pchaigno]

This typo is currently resulting in an error at grammar compilation for GitHub.com (see github-linguist/linguist#3924 for further details). @leodemoura @soonhokong Did one of you find time to look into this?

PS: The online Lightshow app may help if you need to run quick tests but don't have TextMate at hand.