Clones a private or public git project, so you don't have
to remember the long URL. Use
.../git-clone git-tools
for some value of "git-tools"
--- /dev/null
+#!/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 "Could not check out $PROJ"
+