projects
/
git-tools-moved-to-github.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
(from parent 2:
4fa5a3a
)
Merge branch 'master' of ssh://git.indexdata.com:222/home/git/pub/git-tools
author
Heikki Levanto
<heikki@indexdata.dk>
Tue, 29 Sep 2015 12:36:14 +0000
(14:36 +0200)
committer
Heikki Levanto
<heikki@indexdata.dk>
Tue, 29 Sep 2015 12:36:14 +0000
(14:36 +0200)
id-clone
[new file with mode: 0755]
patch
|
blob
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"
+