max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-05 06:57:28 -07:00
parent fde8d35bbb
commit 34f3fcdee5
1 changed files with 0 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/interactive/completionOption.lean.expected.out
View file

@ -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},