id-clone

   1 #!/bin/bash
   2 # A simple script to clone a ID git project
   3 # because I never remember the long URLs
   4
   5
   6 PROJ=$1
   7 URL="ssh://git.indexdata.com:/home/git"
   8
   9 # Try private project first, then public
  10 #
  11 (
  12     echo "Cloning $URL/private/$PROJ"
  13     git clone "$URL/private/$PROJ"
  14 ) ||
  15 (
  16     echo "That did not work"
  17     echo
  18     echo "Cloning $URL/pub/$PROJ"
  19     git clone "$URL/pub/$PROJ"
  20
  21 ) ||
  22 (
  23     echo
  24     echo "Could not check out $PROJ"
  25 )