From 8f80d2c2e0441b7ead0fe9dd889375c1180b2c68 Mon Sep 17 00:00:00 2001
From: maxwell3025 <44588341+maxwell3025@users.noreply.github.com>
Date: Tue, 16 Dec 2025 05:47:33 -0500
Subject: [PATCH] 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
---
 src/lake/schemas/lakefile-toml-schema.json | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/lake/schemas/lakefile-toml-schema.json b/src/lake/schemas/lakefile-toml-schema.json
index 09f40a55d5..6b8ce374cf 100644
--- a/src/lake/schemas/lakefile-toml-schema.json
+++ b/src/lake/schemas/lakefile-toml-schema.json
@@ -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": {