2 # A simple script to clone a ID git project
3 # because I never remember the long URLs
7 URL="ssh://git.indexdata.com:/home/git"
9 # Try private project first, then public
12 echo "Cloning $URL/private/$PROJ"
13 git clone "$URL/private/$PROJ"
16 echo "That did not work"
18 echo "Cloning $URL/pub/$PROJ"
19 git clone "$URL/pub/$PROJ"
24 echo "Could not check out $PROJ"