From 821b1c2b6cf78a676810964879fecbc702e9999a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 31 Aug 2020 16:38:39 -0700
Subject: [PATCH] chore: remove arity

@Kha I improved the arity calculation for `extern`s.
---
 src/Lean/PrettyPrinter/Formatter.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index cc98460872..9f125eaab7 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -185,7 +185,7 @@ p1 <|> p2
 -- Note that there is a mutual recursion
 -- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere
 -- anyway.
-@[extern 8 "lean_mk_antiquot_formatter"]
+@[extern "lean_mk_antiquot_formatter"]
 constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Formatter :=
 arbitrary _