2024-11-18 10:26:37 +00:00
|
|
|
#!/bin/bash -e
|
|
|
|
|
|
|
|
|
|
mkdir -p "$HOME/.ssh"
|
|
|
|
|
echo "$INPUT_SSH_PRIV" > "$HOME/.ssh/id_ed25519"
|
|
|
|
|
echo "$INPUT_KNOWN_HOSTS" > "$HOME/.ssh/known_hosts"
|
2024-11-18 10:44:56 +00:00
|
|
|
chmod 600 "$HOME/.ssh/id_ed25519"
|
2024-11-18 10:26:37 +00:00
|
|
|
|
2024-11-18 11:16:45 +00:00
|
|
|
URL="${GITHUB_SERVER_URL/\/\//\/\/$GITHUB_REPOSITORY_OWNER:$INPUT_TOKEN@}/$GITHUB_REPOSITORY"
|
|
|
|
|
|
2024-11-18 11:23:18 +00:00
|
|
|
git init -b main
|
2024-11-18 11:16:45 +00:00
|
|
|
git remote add origin "$URL"
|
2024-11-18 11:28:00 +00:00
|
|
|
git remote set-url --push origin "$INPUT_URL"
|
2024-11-18 11:16:45 +00:00
|
|
|
git fetch -pP
|
2024-11-18 11:25:16 +00:00
|
|
|
git push origin --mirror
|
