From ada6661f32cabd6131194e90280d3ed5bba2d635 Mon Sep 17 00:00:00 2001
From: Heikki Levanto <heikki@indexdata.dk>
Date: Tue, 29 Sep 2015 14:35:04 +0200
Subject: [PATCH] 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"
---
 id-clone |   23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100755 id-clone

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