Added a script id-clone
authorHeikki Levanto <heikki@indexdata.dk>
Tue, 29 Sep 2015 12:35:04 +0000 (14:35 +0200)
committerHeikki Levanto <heikki@indexdata.dk>
Tue, 29 Sep 2015 12:35:04 +0000 (14:35 +0200)
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 [new file with mode: 0755]

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