[PPL-devel] [GIT] ppl/w3ppl(master): Fetch only specified branch and without history.

[Abramo Bagnara]

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

Author: Abramo Bagnara <abramo.bagnara at gmail.com>
Date:   Tue Apr  7 18:51:37 2009 +0200

Fetch only specified branch and without history.

---

 bin/ppl_release |   11 +++++++++--
 1 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/bin/ppl_release b/bin/ppl_release
index f0219ba..856d715 100755
--- a/bin/ppl_release
+++ b/bin/ppl_release
@@ -92,8 +92,15 @@ build_sources() {
   # and version strings are updated.
   if [ ${FINAL} -ne 0 ]; then
     inform "Updating ChangeLogs and version files"
-    ${GIT} clone ${GITROOT} ${SOURCE_DIRECTORY} || \
-	error "Could not clone release sources"
+#     ${GIT} clone ${GITROOT} ${SOURCE_DIRECTORY} || \
+# 	error "Could not clone release sources"
+    mkdir ${SOURCE_DIRECTORY}
+    (changedir ${SOURCE_DIRECTORY}
+	${GIT} init
+	${GIT} remote add origin ${GITROOT} -t ${BRANCH} -m ${BRANCH}
+	${GIT} fetch --depth=1) || \
+	    error "Could not clone release sources"
+#
     (changedir ${SOURCE_DIRECTORY}
 	${GIT} checkout --track -b ${BRANCH} origin/${BRANCH}) || \
 	    error "Could not checkout ${BRANCH}"