[PPL-devel] [GIT] ppl/w3ppl(master): Updated.

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Sun Feb 20 14:57:00 2011 +0100

Updated.

---

 bin/update_web_site |   94 ++++++++++----------------------------------------
 1 files changed, 19 insertions(+), 75 deletions(-)

diff --git a/bin/update_web_site b/bin/update_web_site
index d8268b6..5b1b4d6 100755
--- a/bin/update_web_site
+++ b/bin/update_web_site
@@ -9,15 +9,8 @@ BRANCH=ppl-0_11-branch
 
 export PATH=/usr/local/bin:$PATH
 
-# Where the repository is on cvs.cs.unipr.it.
-local_repository=/git/ppl
-
-# Where the repository is for remote developers.
-#remote_repository=$USER at cvs.cs.unipr.it:$local_repository
-remote_repository=ssh://bagnara@git.cs.unipr.it$local_repository
-
-# The local machine.
-machine=`uname -n`
+# Where the repository is.
+remote_repository=ssh://git@git.cs.unipr.it/ppl/ppl
 
 # The local directory used for building the documentation.
 top_dir=/tmp/w3ppl-update.$$
@@ -25,25 +18,10 @@ top_dir=/tmp/w3ppl-update.$$
 # The destination directory in the web area.
 dest_dir=/var/www/html/local/ppl
 
-# The email addresses of the developers.
-case "$machine" in
-    zoltan.unisuv.it)
-	developers="roberto"
-        java_dir=/usr/java/default
-	;;
-    charlie.cs.unipr.it)
-	developers="zaffanella"
-        java_dir=/usr/lib/jvm/java-openjdk
-	;;
-    *)
-#	developers="roberto"
-	developers="bagnara at cs.unipr.it"
-#       java_dir=/usr/java/default
-#	developers="ppl-devel at cs.unipr.it"
-    	;;
-esac
-
-# File where the notifications for developers are collected.
+# The email addresses of the person(s) to be notified.
+developers="bagnara at cs.unipr.it"
+
+# File where the notifications are collected.
 notification=$top_dir/notification
 
 # Lock file name.
@@ -62,52 +40,18 @@ fetch_branch() {
 }
 
 obtain_sources() {
-    case "$machine" in
-    spartacus.cs.unipr.it)
-	fetch_branch $local_repository w3ppl master
-	if [ $? -ne 0 ]
-	then
-	    echo "Cannot copy the PPL web pages." >>$notification
-	    maybe_notify_developers_and_exit
-	fi
-	fetch_branch $local_repository ppl $BRANCH
-	if [ $? -ne 0 ]
-	then
-	    echo "Cannot export the PPL sources." >>$notification
-	    maybe_notify_developers_and_exit
-	fi
-	;;
-    zoltan.unisuv.it)
-	cp -r $HOME/ppl/*ppl .
-	if [ $? -ne 0 ]
-	then
-	    echo "Cannot copy the PPL sources or web pages." >>$notification
-	    maybe_notify_developers_and_exit
-	fi
-	;;
-    charlie.cs.unipr.it)
-	cp -r $HOME/cvs-stuff/*ppl .
-	if [ $? -ne 0 ]
-	then
-	    echo "Cannot copy the PPL sources or web pages." >>$notification
-	    maybe_notify_developers_and_exit
-	fi
-	;;
-    *)
-	fetch_branch $remote_repository w3ppl master
-	if [ $? -ne 0 ]
-	then
-	    echo "Cannot export the PPL web pages." >>$notification
-	    maybe_notify_developers_and_exit
-	fi
-	fetch_branch $remote_repository ppl $BRANCH
-	if [ $? -ne 0 ]
-	then
-	    echo "Cannot export the PPL sources." >>$notification
-	    maybe_notify_developers_and_exit
-	fi
-    	;;
-    esac
+    fetch_branch $remote_repository w3ppl master
+    if [ $? -ne 0 ]
+    then
+	echo "Cannot export the PPL web pages." >>$notification
+	maybe_notify_developers_and_exit
+    fi
+    fetch_branch $remote_repository ppl $BRANCH
+    if [ $? -ne 0 ]
+    then
+	echo "Cannot export the PPL sources." >>$notification
+	maybe_notify_developers_and_exit
+    fi
 }
 
 maybe_notify_developers_and_exit() {
@@ -153,7 +97,7 @@ obtain_sources
 
 # Make and install the w3ppl documentation.
 cd $top_dir/w3ppl/htdocs
-make DESTDIR=$dest_dir
+make -k DESTDIR=$dest_dir
 
 # Create a build directory.
 mkdir $top_dir/build