[PPL-devel] [GIT] ppl/w3ppl(master): Unwanted command commented out.

14 Apr 2009

Module: ppl/w3ppl
Branch: master
Commit: 2be4422419dcb77f535893d3839e827be05ef8a0
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=2be4422419d...
Author: Roberto Bagnara bagnara@cs.unipr.it
Date:   Tue Apr 14 11:23:44 2009 +0200
Unwanted command commented out.
---
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 802a55a..24e030b 100755
--- a/bin/update_web_site
+++ b/bin/update_web_site
@@ -226,7 +226,7 @@ make -j 8 >&MAKELOG.library
 # fi
# Build the doxygen documentation.
-cd ../../doc
+#cd ../../doc
 cd doc
 make world >&MAKELOG.documentation

    