Add only the origin remote to the local project

create_local_project no longer adds a github remote, with or without GitHub:
a push to origin reaches GitHub through the push mirror. A github remote that
already exists, such as one made by an earlier version, is left as it is, and
a different origin is still refused.

- Remove github_remote_url, which nothing else used
- README describes the one remote and how to remove an old github remote
- Tests: origin is the only remote with and without GitHub, no GitHub address
  in .git/config, and an existing github remote is kept

Task: MIL-008#1
Task: MIL-008#2
Task: MIL-008#3
This commit is contained in:
2026-10-08 11:13:21 +08:00
parent 039a28c01b
commit 79f6edeb38
4 changed files with 36 additions and 24 deletions
+4 -5
View File
@@ -71,8 +71,10 @@ checkout_gitea_history() {
fi
}
# create_local_project: the directory, the git repository on main, the
# remotes and, when a license applies, the license history. No commit is made.
# create_local_project: the directory, the git repository on main, the origin
# remote and, when a license applies, the license history. No commit is made.
# Gitea is the only remote: a push to it reaches GitHub through the push
# mirror, so no github remote is added (and none that exists is removed).
create_local_project() {
local label="Local project" dir="${PROJECT[directory]}"
begin_step "$label"
@@ -82,9 +84,6 @@ create_local_project() {
git_project "$dir" symbolic-ref HEAD "refs/heads/$DEFAULT_BRANCH"
fi
ensure_remote "$dir" origin "$(origin_url)"
if ((PROJECT[has_github])); then
ensure_remote "$dir" github "$(github_remote_url)"
fi
if [[ -n ${PROJECT[license]} ]]; then
checkout_gitea_history "$dir"
fi