projects
/
ctsim.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
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}
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
echo "Making documentation"
pushd doc
make all