blob: 1c56d1dacb8694e254381527d2ee39ba1d0bd94c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
# vim: ft=sh
[ -n "$LAMINAR_COMMON" ] # variables definition guard
V="${V:-0}"
if [ "$V" -ge 3 ]; then
set -x
fi
## Simple echo wrappers #########################################################
echo_stage() {
echo -e "\033[1;34m========== " "$@" " ==========\033[0m ($(date))" >&2
}
echo_info() {
echo -e "\033[1;32m---------- " "$@" " ----------\033[0m" >&2
}
echo_debug() {
echo -e "\033[1;30m--- " "$@" " ---\033[0m" >&2
}
echo_fail() {
echo -e "\033[1;31m---------- " "$@" " ----------\033[0m" >&2
return 1
}
## GIT ##########################################################################
# Fetch bare git repository
# First argument has to be a source URL
# Second argument is path to directory to which will be repository cloned to.
git_fetch_bare() {
if [ -d "$2" ]; then
git --git-dir="$2" --bare remote update --prune
else
git clone --mirror "$1" "$2"
fi
}
# Common function for git_fetch_{w,g}
# Additional fourth argument should be base path to git mirror
_git_fetch() {
local BRANCH="$3"
[ -n "$BRANCH" ] || BRANCH=master
git_fetch_bare "$1" "$4/$2"
git --git-dir="$4/$2" --bare worktree prune # remove old work trees
git --git-dir="$4/$2" --bare worktree add --force --detach "$2" "$BRANCH"
}
# Fetch git repository with mirror
# _w: mirror is in WORKSPACE
# _t: mirror is in TWORKSPACE
# _g: mirror is in global workspace
# First agument has to be a source URL
# Second argument is name of directory to which will be directory cloned in.
# Second argument is optional and should be branch name (master is used if not
# provided).
git_fetch_w() {
_git_fetch "$1" "$2" "$3" "$WORKSPACE/git-mirror"
}
git_fetch_t() {
_git_fetch "$1" "$2" "$3" "$TWORKSPACE/git-mirror"
}
git_fetch_g() {
_git_fetch "$1" "$2" "$3" "$HOME/workspace/git-mirror"
}
# Clones one depth given repository with given branch/tag/hash
# First agument has to be a source URL
# Second argument is name of directory to which will be directory cloned in.
# Second argument is optional and should be branch name (master is used if not
# provided).
git_clone() {
local BRANCH="$3"
[ -n "$BRANCH" ] || BRANCH=master
(
mkdir "$2"
cd "$2"
git init
git remote add origin "$1"
git fetch --depth 1 origin "$BRANCH"
git checkout FETCH_HEAD
)
}
|
