#! /bin/bash
# Last edited on 2025-07-31 12:19:01 by stolfi

# Uploads the current directory to the corresponding GitHub backage.

repo="$1"; shift # Repository on Github, e.g. "JSLIBS".]
branch="$1"; shift # Branch for push, either "main" or "origin" or who knows.
message="$*"
if [[ "/${message}" == "/" ]]; then 
  echo "** must provide a commit message" 1>&2; exit 1
fi

url="git@github.com:JorgeStolfi/${repo}.git"
echo "url = ${url}" 1>&2

git switch ${branch}

git add --verbose --update

git commit --verbose -m "${message}"

git push --verbose "${url}" ${branch}