r1942: *** empty log message ***

[ctsim.git] / make-dist.sh

diff --git a/make-dist.sh b/make-dist.sh
index 5dbf430f6a14b994a96797fa16d3296128a64e1b..5ab5bf3a56e90ea0139808556379422ba0936c7d 100755 (executable)
--- a/make-dist.sh
+++ b/make-dist.sh
@@ -13,7 +13,7 @@ TOPDIR=`basename $PWD`
 DISTDIR=${PKG}-${VERSION}
 DEBDIR=${DEBPKG}-${VERSION}
 
-if [! (-f docs/${PKG}.htb -a -f docs/html/${PKG}_contents.html -a -f docs/${PKG}.pdf) ]; then
+if [! -f docs/${PKG}.htb -o ! -f docs/html/${PKG}_contents.html -o ! -f docs/${PKG}.pdf ]; then
   echo "Making documentation"
   pushd doc
   make all