> Didn't you already push it? It appeared in my git tree, but maybe > I committed it locally but forgot about it? > > If it's already pushed, you'll need to make a new patch against > master; go ahead and push that.
Hi Graham, I don't think I have write permissions in the git repository so if it has been pushed it's from Carl. Frédéric _______________________________________________ lilypond-user mailing list lilypond-user@gnu.org http://lists.gnu.org/mailman/listinfo/lilypond-user
