Module: ppl/w3ppl Branch: master Commit: a7cde6c37d0364228688f7ac622091ce474c375b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=a7cde6c37d0...
Author: Roberto Bagnara bagnara@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@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@cs.unipr.it" -# java_dir=/usr/java/default -# developers="ppl-devel@cs.unipr.it" - ;; -esac - -# File where the notifications for developers are collected. +# The email addresses of the person(s) to be notified. +developers="bagnara@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