- Fixed typo

This commit is contained in:
Dave M. 2023-10-17 17:27:17 +00:00
parent 406694ce51
commit 74d88dc8bf
1 changed files with 1 additions and 1 deletions

View File

@ -20,7 +20,7 @@
"extra" : {
"lean" : {
"autoload": {
"definition" : [
"definitions" : [
{ "\\Lean\\Console\\Lean" : "definitions" }
]
}