Fix the creation of public releases

When the release names of consecutive public releases are the identical,
there was a bug:
"gzip: CGAL-4.4-dev.tar.gz already exists;       not overwritten"
This commit is contained in:
Laurent Rineau
2014-02-18 15:56:52 +01:00
parent c2c472b20b
commit a5cc4dc910
@@ -316,6 +316,7 @@ if [ -n "$DO_PUBLIC" ]; then
# popd
# cp -a doc_html/* ${public_release_name}/doc_html
rm -f "${public_release_name}".tar*
tar -cf "${public_release_name}.tar" "${public_release_name}"
mkdir "${HTML_DIR}/${release_name}-public"
xz --best "${public_release_name}.tar" -c > "${HTML_DIR}/${release_name}-public/${public_release_name}.tar.xz"