+Note that when you push BRANCH from SUBDIR to the main repository,
+and BRANCH is checked out in the main repository, you must save
+uncommitted changes (see SOME GIT TIPS) and do 'git reset --hard' in
+the main repository in order to apply pushed changes in the working
+tree of the main repository.
+
+
+GIT PUSH ACCESS
+
+If you have permission to push to Git with login USER, please start a
+new Git repository from scratch to avoid polluting history with
+duplicate commits; follow the usual instructions, except that every
+file you write in .git/remotes should contain instead
+
+URL: ssh://USER@git.sv.gnu.org/srv/git/lilypond.git
+Push: BRANCH:refs/heads/BRANCH
+Pull: BRANCH:refs/remotes/origin/BRANCH
+
+Then, you can use .git/remotes/NAME to push BRANCH with
+
+ git push NAME
+
+which works regardless of the branch checked out.
+