author | wenzelm |
Tue, 21 Jul 1998 17:30:13 +0200 | |
changeset 5172 | 0af867c248ee |
parent 5171 | cca9a908c270 |
child 5173 | 5e68e3cb1f60 |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- a/Admin/makedist Tue Jul 21 16:43:38 1998 +0200 +++ b/Admin/makedist Tue Jul 21 17:30:13 1998 +0200 @@ -124,7 +124,8 @@ find . -name CVS -exec rm -rf {} \; -find Doc \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) -exec mv {} Distribution/doc \; +find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) \) \ + -exec mv -f {} Distribution/doc \; rm Distribution/doc/Isa-logics.eps cp Admin/index.html $DISTBASE rm -rf Admin Doc