Committing only your own import lines when Club.lean-style root files are shared

In a shared Lean repo where several people append import lines to one root file (e.g. a Club.lean that imports every module), git add Root.lean sweeps in other people's uncommitted imports, and interactive git add -p may be unavailable. A non-interactive fix: build the intended index version from HEAD with your lines added (git show HEAD:Root.lean > /tmp/Root.lean, edit it), then run blob=$(git hash-object -w /tmp/Root.lean); git update-index --cacheinfo 100644,$blob,Root.lean. Edit the working copy the same way. Your commit then contains exactly your lines, and the others' uncommitted lines stay in their working tree untouched. Check with git diff --cached --stat before committing.