From 34f3fcdee53baaf47083390d7816de2859dc3156 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 5 Sep 2022 06:57:28 -0700 Subject: [PATCH] chore: fix test --- .../interactive/completionOption.lean.expected.out | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/tests/lean/interactive/completionOption.lean.expected.out b/tests/lean/interactive/completionOption.lean.expected.out index b0813d9f12..8779bfa71c 100644 --- a/tests/lean/interactive/completionOption.lean.expected.out +++ b/tests/lean/interactive/completionOption.lean.expected.out @@ -234,18 +234,6 @@ "kind": 10, "detail": "(false), enable/disable tracing for the given module and submodules"}, - {"textEdit": - {"replace": - {"start": {"line": 10, "character": 11}, - "end": {"line": 10, "character": 18}}, - "newText": "trace.Compiler.simp.projInst", - "insert": - {"start": {"line": 10, "character": 11}, - "end": {"line": 10, "character": 18}}}, - "label": "trace.Compiler.simp.projInst", - "kind": 10, - "detail": - "(false), enable/disable tracing for the given module and submodules"}, {"textEdit": {"replace": {"start": {"line": 10, "character": 11},