Admin/makedist
changeset 6630 5f810292c030
parent 6304 9a82e1c3d9da
child 6748 f1f70344b749
--- a/Admin/makedist	Mon May 10 17:44:17 1999 +0200
+++ b/Admin/makedist	Mon May 10 17:45:16 1999 +0200
@@ -110,11 +110,13 @@
 # make docs
 
 cd $DISTBASE/$DISTNAME/Doc
+PDFLATEX=$(type -path pdflatex)
 
 for DOC in $(cat Contents)
 do
   cd $DOC
-  make dist
+  make dvi
+  [ -n "$PDFLATEX" ] && make clean pdf
   cd ..
 done
 
@@ -123,8 +125,9 @@
 
 cd $DISTBASE/$DISTNAME
 
-find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) \) \
-  -exec mv -f {} Distribution/doc \;
+MOVE=$(find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) \) \
+  | grep -v 'gfx/.*pdf')
+mv -f $MOVE Distribution/doc
 rm Distribution/doc/Isa-logics.eps
 cp Admin/index.html $DISTBASE
 rm -rf Admin Doc