Admin/lib/Tools/build_doc

--- a/Admin/lib/Tools/build_doc	Tue Aug 28 19:24:32 2012 +0200
+++ b/Admin/lib/Tools/build_doc	Tue Aug 28 20:10:53 2012 +0200
@@ -84,9 +84,9 @@
 if [ "$RC" = 0 ]; then
   for FILE in $(find "$OUTPUT" -name "*.eps" -o -name "*.ps")
   do
-    mv -f "$FILE" "$ISABELLE_HOME/doc"
+    cp -f "$FILE" "$ISABELLE_HOME/doc"
   done
-  mv -f "$OUTPUT"/*.dvi "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc"
+  cp -f "$OUTPUT"/*.dvi "$OUTPUT"/*.pdf "$ISABELLE_HOME/doc"
 fi
 
 rm -rf "$OUTPUT"