Added a script id-clone

[git-tools-moved-to-github.git] / id-clone

diff --git a/id-clone b/id-clone
new file mode 100755 (executable)
index 0000000..67632ec
--- /dev/null
+++ b/id-clone
@@ -0,0 +1,23 @@
+#!/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"
+