mirror of
https://github.com/Dev-Wiki/git-repo.git
synced 2026-06-23 02:45:39 +08:00
a0de6e8eab
It hasn't been necessary for a long time, and its functionality can be accomplished with 'git push'. Change-Id: Ic00d3adbe4cee7be3955117489c69d6e90106559