equal
deleted
inserted
replaced
163 EOF |
163 EOF |
164 |
164 |
165 MOVE=$($FIND Doc \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf') |
165 MOVE=$($FIND Doc \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf') |
166 mv -f $MOVE Distribution/doc |
166 mv -f $MOVE Distribution/doc |
167 rm Distribution/doc/Isa-logics.eps |
167 rm Distribution/doc/Isa-logics.eps |
168 rm -rf Doc Tools |
168 rm -rf Doc |
169 |
169 |
170 mkdir src contrib |
170 mkdir src contrib |
171 mv $SRCS src |
171 mv $SRCS src |
172 |
172 |
173 mv Distribution/* . |
173 mv Distribution/* . |