Microsoft/vscode
Voir sur GitHubGit - Respect submodule names defined in superrepo's `.gitmodules` file
Open
#269 812 ouverte le 4 oct. 2025
feature-requestgithelp wanted
Métriques du dépôt
- Stars
- (74 848 stars)
- Métriques de merge PR
- (Merge moyen 11h 43m) (1 000 PRs mergées en 30 j)
Description
In the superrepo, with the following .git/config
[core]
repositoryformatversion = 0
filemode = false
bare = false
logallrefupdates = true
symlinks = false
ignorecase = true
[remote "origin"]
url = https://github.com/Gravifer/lean-mathlib-1stproj.git
fetch = +refs/heads/*:refs/remotes/origin/*
[branch "main"]
remote = origin
merge = refs/heads/main
vscode-merge-base = origin/main
[submodule "mil"]
url = https://github.com/Gravifer/lean-comm.mathematics_in_lean.git
active = true
[submodule "mpil"]
url = https://github.com/leanprover-community/lean4-metaprogramming-book.git
active = true
and .gitmodules
[submodule "mil"]
path = LeanMathlib1stproj/mil
url = https://github.com/Gravifer/lean-comm.mathematics_in_lean.git
[submodule "mpil"]
path = LeanMathlib1stproj/mpil/foo
url = https://github.com/leanprover-community/lean4-metaprogramming-book.git
The SCM panel shows the second submodule with the name foo, as it determines the name using only the submodule root dirname (impressing skimming the source code). Upon the situation where the tags have been customized, it can be more informant to use the configured tag; the behavior can be left unaltered should the tag is left auto-generated, as it would just be the relative path to the submodule root.