[PPL-devel] [GIT] ppl/w3ppl(master): Two corrections concerning the location of the Git repositories.

[Roberto Bagnara]

Module: ppl/w3ppl
Branch: master
Commit: e193e773cc920a1d2b3a8f00d48ede443e9f2fa5
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=e193e773cc920a1d2b3a8f00d48ede443e9f2fa5

Author: Roberto Bagnara <bagnara at 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)
 }