From f92166e9135e2077d9f548a8485bfb99b02a9912 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Jun 2020 16:43:44 -0700 Subject: [PATCH] chore: fix test --- tests/lean/run/termParserAttr.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean index ae030c7911..0fb5ecfd02 100644 --- a/tests/lean/run/termParserAttr.lean +++ b/tests/lean/run/termParserAttr.lean @@ -16,7 +16,7 @@ open Lean.Parser @[termParser] def tst := parser! "(|" >> termParser >> optional (symbol ", " >> termParser) >> "|)" @[termParser] def boo : ParserDescr := -ParserDescr.node `boo +ParserDescr.node `boo 10 (ParserDescr.andthen (ParserDescr.symbol "[|") (ParserDescr.andthen