From: Heikki Levanto <heikki@indexdata.dk>
Date: Tue, 29 Sep 2015 12:36:14 +0000 (+0200)
Subject: Merge branch 'master' of ssh://git.indexdata.com:222/home/git/pub/git-tools
X-Git-Url: http://git.indexdata.com/?p=git-tools-moved-to-github.git;a=commitdiff_plain;h=4d1d642b47e16e1a45b712b8bf6484f853fbdd50;hp=4fa5a3ae2d26663ebc81ab0d6fbe9dcf57174c50

Merge branch 'master' of ssh://git.indexdata.com:222/home/git/pub/git-tools
---

diff --git a/id-clone b/id-clone
new file mode 100755
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"
+