Microsoft/vscode
Vedi su GitHubGit - Respect submodule names defined in superrepo's `.gitmodules` file
Open
#269.812 aperta il 4 ott 2025
feature-requestgithelp wanted
Metriche repository
- Star
- (74.848 star)
- Metriche merge PR
- (Merge medio 11h 43m) (1000 PR mergiate in 30 g)
Descrizione
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.