Admin/makedist
changeset 16481 fe61cdf5af51
parent 16328 49c1f9dedc56
child 16508 5e5945ae284c
equal deleted inserted replaced
16480:abf475cf11f2 16481:fe61cdf5af51
   174 # this is a generated file - do not edit unless you know what you are doing
   174 # this is a generated file - do not edit unless you know what you are doing
   175 
   175 
   176 DISTNAME=$DISTNAME
   176 DISTNAME=$DISTNAME
   177 EOF
   177 EOF
   178 
   178 
   179 MOVE=$($FIND Doc \( -type f -a -not -type l -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
   179 MOVE=$($FIND Doc \( -type f -a -not -type l -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
   180 mv -f $MOVE Distribution/doc
   180 mv -f $MOVE Distribution/doc
   181 rm Distribution/doc/Isa-logics.eps
   181 rm Distribution/doc/Isa-logics.eps
   182 rm -rf Doc Tools
   182 rm -rf Doc Tools
   183 
   183 
   184 mkdir src contrib
   184 mkdir src contrib