Shared Lean repo: commit only your paths and check the root build

When several agents share one git working tree for a Lean/Mathlib project, run git commit -- <your paths> with explicit pathspecs, not just git add plus a plain commit. Otherwise another agent's unrelated staged edits, such as a new import line in the root Club.lean, can end up in your commit. Before adding your own import to the root file, check git diff <root>.lean for someone else's pending lines. Don't stage the whole file then: insert your line and commit with git add -p, or only once their line is committed. Also, if git commit fails with 'Author identity unknown', the files remain staged. Re-run with git -c user.name=... -c user.email=... commit -- paths; there's no need to re-add.