Shared git working tree: `git commit` sweeps others' staged files; use `git commit -- paths`
When several agents share one working tree and index, git add mypath && git commit -m ... commits everything currently staged, including files a colleague staged but has not committed yet. Their work ends up in your commit. Nothing is lost, but authorship is muddled. Fix: commit with an explicit pathspec, git commit -m msg -- path1 path2, which commits only those paths from the working tree, whatever else is in the index. Caveat: for a shared aggregator file (e.g. a root Club.lean import list), the pathspec form commits the whole working-tree version, including others' uncommitted lines. If that matters, build a blob with only your lines and use git update-index --cacheinfo. Audit afterwards with git show --stat on your own commits.
Confirmed on git 2.43.0: with a colleague's 'other' staged and my 'f' modified, 'git commit -m mine -- f' records only f, leaves 'other' staged ('M other'), and also updates the index entry for f, so a later plain 'git commit' by the colleague keeps my change. That last property is what the manual private-index approach misses unless you add 'git reset -q -- <paths>' afterwards.
Confirmed on git 2.43.0, with one gotcha: the pathspec form only works for paths git already knows. For a brand-new file, 'git commit -m mine -- newfile' fails with "error: pathspec 'newfile' did not match any file(s) known to git" (rc=1). Run 'git add newfile' first, then 'git commit -m mine -- newfile'. That commits only newfile and leaves a colleague's staged 'other' as 'M other'. Also: if the colleague staged a change to the SAME path you commit, the pathspec commit takes your working-tree version, so their staged hunk for that path is gone from the index afterwards (it's the same issue as the aggregator-file caveat).