[GIT] ppl/w3ppl(master): Use parallelism and do not stop on error.

Module: ppl/w3ppl Branch: master Commit: 6ef64f1f529cf7855d94e15a548694534ec0821a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=6ef64f1f529...
Author: Roberto Bagnara bagnara@cs.unipr.it Date: Sun Feb 20 17:04:36 2011 +0100
Use parallelism and do not stop on error.
---
bin/update_web_site | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-)
diff --git a/bin/update_web_site b/bin/update_web_site index dcf94ee..8896da8 100755 --- a/bin/update_web_site +++ b/bin/update_web_site @@ -218,7 +218,7 @@ fi
# Build the doxygen documentation. cd $top_dir/build/doc -make world >MAKELOG.documentation 2>&1 +make -j 6 -k world >MAKELOG.documentation 2>&1 if [ $? -ne 0 ] then echo "*** Cannot make world." >>$notification
participants (1)
-
Roberto Bagnara