Admin/makedist
changeset 3281 d4ddd43f418a
parent 3257 4e3724e0659f
child 3305 d8114e93ef66
--- a/Admin/makedist	Wed May 21 17:21:46 1997 +0200
+++ b/Admin/makedist	Wed May 21 17:31:12 1997 +0200
@@ -122,7 +122,7 @@
 find . -name CVS -exec rm -rf {} \;
 
 mkdir -p Tools/8bit/bin    #FIXME tmp
-find Doc -name \*.dvi -o -name \*.eps -o \*.ps -exec mv {} Distribution/doc \;
+find Doc -name \*.dvi -o -name \*.eps -o -name \*.ps -exec mv {} Distribution/doc \;
 rm -rf Admin Doc
 
 mkdir src