fix: add table variant for require.git field in lakefile.toml schema (#11536)
This PR corrects the JSON Schema at `src/lake/schemas/lakefile-toml-schema.json` to allow the table variant of the `require.git` field in `lakefile.toml` as specified in the [reference](https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/#Lake___Dependency-git). Closes #11535
This commit is contained in:
parent
fd0a65f312
commit
8f80d2c2e0
1 changed files with 2 additions and 1 deletions
|
|
@ -355,7 +355,8 @@
|
|||
"description": "A dependency on the local filesystem, specified by its path."
|
||||
},
|
||||
"git": {
|
||||
"type": "string",
|
||||
"type": ["string", "object"],
|
||||
"default": "",
|
||||
"description": "A dependency in a Git repository, specified by its URL."
|
||||
},
|
||||
"subDir": {
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue