Module: ppl/w3ppl Branch: master Commit: e193e773cc920a1d2b3a8f00d48ede443e9f2fa5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=e193e773cc9...
Author: Roberto Bagnara bagnara@cs.unipr.it Date: Sun Feb 20 15:10:17 2011 +0100
Two corrections concerning the location of the Git repositories.
---
bin/update_web_site | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/bin/update_web_site b/bin/update_web_site index 5b1b4d6..3c8db83 100755 --- a/bin/update_web_site +++ b/bin/update_web_site @@ -10,7 +10,7 @@ BRANCH=ppl-0_11-branch export PATH=/usr/local/bin:$PATH
# Where the repository is. -remote_repository=ssh://git@git.cs.unipr.it/ppl/ppl +remote_repository=ssh://git@git.cs.unipr.it/ppl
# The local directory used for building the documentation. top_dir=/tmp/w3ppl-update.$$ @@ -34,7 +34,7 @@ fetch_branch() { mkdir $module && (cd $module && git init && - git remote add origin $repo/$module.git -t $branch -m $branch && + git remote add origin $repo/$module -t $branch -m $branch && git fetch --depth=1 && git checkout --track -b $branch origin/$branch) }