From: Heikki Levanto <heikki@indexdata.dk>
Date: Tue, 29 Sep 2015 12:35:04 +0000 (+0200)
Subject: Added a script id-clone
X-Git-Url: http://git.indexdata.com/?p=git-tools-moved-to-github.git;a=commitdiff_plain;h=ada6661f32cabd6131194e90280d3ed5bba2d635

Added a script id-clone

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"
---

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"
+