Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
  • Issue/1788-extractionCronjob
  • Issue/1792-newMetadataStructure
  • Issue/2518-docs
  • Issue/2769-migrateCron
  • dev
  • gitkeep
  • main
  • test
  • v0.1.0
  • v0.1.1
  • v0.1.10
  • v0.1.11
  • v0.1.2
  • v0.1.3
  • v0.1.4
  • v0.1.5
  • v0.1.6
  • v0.1.7
  • v0.1.8
  • v0.1.9
20 results

Target

Select target project
  • coscine/backend/scripts/metadataextractorcron
1 result
Select Git revision
  • Issue/1788-extractionCronjob
  • Issue/1792-newMetadataStructure
  • Issue/2518-docs
  • Issue/2769-migrateCron
  • dev
  • gitkeep
  • main
  • test
  • v0.1.0
  • v0.1.1
  • v0.1.10
  • v0.1.11
  • v0.1.2
  • v0.1.3
  • v0.1.4
  • v0.1.5
  • v0.1.6
  • v0.1.7
  • v0.1.8
  • v0.1.9
20 results
Show changes
#!/bin/sh
# ref: https://help.github.com/articles/adding-an-existing-project-to-github-using-the-command-line/
#
# Usage example: /bin/sh ./git_push.sh wing328 openapi-petstore-perl "minor update" "gitlab.com"
git_user_id=$1
git_repo_id=$2
release_note=$3
git_host=$4
if [ "$git_host" = "" ]; then
git_host="github.com"
echo "[INFO] No command line input provided. Set \$git_host to $git_host"
fi
if [ "$git_user_id" = "" ]; then
git_user_id="GIT_USER_ID"
echo "[INFO] No command line input provided. Set \$git_user_id to $git_user_id"
fi
if [ "$git_repo_id" = "" ]; then
git_repo_id="GIT_REPO_ID"
echo "[INFO] No command line input provided. Set \$git_repo_id to $git_repo_id"
fi
if [ "$release_note" = "" ]; then
release_note="Minor update"
echo "[INFO] No command line input provided. Set \$release_note to $release_note"
fi
# Initialize the local directory as a Git repository
git init
# Adds the files in the local repository and stages them for commit.
git add .
# Commits the tracked changes and prepares them to be pushed to a remote repository.
git commit -m "$release_note"
# Sets the new remote
git_remote=$(git remote)
if [ "$git_remote" = "" ]; then # git remote not defined
if [ "$GIT_TOKEN" = "" ]; then
echo "[INFO] \$GIT_TOKEN (environment variable) is not set. Using the git credential in your environment."
git remote add origin https://${git_host}/${git_user_id}/${git_repo_id}.git
else
git remote add origin https://${git_user_id}:"${GIT_TOKEN}"@${git_host}/${git_user_id}/${git_repo_id}.git
fi
fi
git pull origin master
# Pushes (Forces) the changes in the local repository up to the remote repository
echo "Git pushing to https://${git_host}/${git_user_id}/${git_repo_id}.git"
git push origin master 2>&1 | grep -v 'To https'