#! /bin/bash
# Last edited on 2024-07-26 17:40:44 by stolfi

repo="$1"; shift # Repository on Github, e.g. "JSLIBS".

# Downloads the current state of repository {repo} to a
# new subfolder called {repo} in the current folder.

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

git clone --verbose "${url}"

# git init