#!/bin/bash
# A simple script to clone a ID git project
# because I never remember the long URLs


PROJ=$1
URL="ssh://git.indexdata.com:/home/git"

# Try private project first, then public
# 
(
    echo "Cloning $URL/private/$PROJ"
    git clone "$URL/private/$PROJ"
) ||
(
    echo "That did not work"
    echo
    echo "Cloning $URL/pub/$PROJ"
    git clone "$URL/pub/$PROJ"

) ||
(
    echo 
    echo "Could not check out $PROJ"
)