summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authortv <tv@shackspace.de>2015-06-28 14:54:46 +0200
committertv <tv@shackspace.de>2015-06-28 14:54:46 +0200
commit3ca8eec45c93d6fd0f887613f7df2b16e63a8b69 (patch)
tree5317f46106401bb46d738e0f1e32f8ed97c9712d
parentf44736bb6c2f6051141bafd7fd88bdea08a02790 (diff)
fetchgit: rev-parse using --verify
-rwxr-xr-xbin/fetchgit6
1 files changed, 3 insertions, 3 deletions
diff --git a/bin/fetchgit b/bin/fetchgit
index ffd7e7426..7862989be 100755
--- a/bin/fetchgit
+++ b/bin/fetchgit
@@ -35,8 +35,8 @@ work_git() {
is_up_to_date() {
test -d "$cache_dir" &&
test -d "$work_dir" &&
- test "$(cache_git rev-parse "$git_rev")" = "$git_rev" &&
- test "$(work_git rev-parse HEAD)" = "$git_rev"
+ test "$(cache_git rev-parse --verify "$git_rev")" = "$git_rev" &&
+ test "$(work_git rev-parse --verify HEAD)" = "$git_rev"
}
# Notice how the remote name "origin" has been chosen arbitrarily.
@@ -54,7 +54,7 @@ if ! is_up_to_date; then
if ! test -d "$work_dir"; then
git clone -n --shared "$cache_dir" "$work_dir"
fi
- commit_name=$(cache_git rev-parse "$git_rev")
+ commit_name=$(cache_git rev-parse --verify "$git_rev")
work_git checkout "$commit_name" -- "$(readlink -f "$work_dir")"
work_git checkout -q "$commit_name"
work_git submodule init