# HG changeset patch
# User wenzelm
# Date 926351116 -7200
# Node ID 5f810292c03053c209d65a4716a4781f8b6652bd
# Parent  6edc66a9d80b582085e59618ad434f45e918e078
make pdf;

diff -r 6edc66a9d80b -r 5f810292c030 Admin/makedist
--- 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