# HG changeset patch
# User wenzelm
# Date 1346177453 -7200
# Node ID f4d4d6d6702b9dc8aa57bbf191c496520fb4c1a2
# Parent  ffb4f2b9b1d3429fdcbb2cac0dc1b1ac7538fa8b
prefer cp over mv, to reduce assumptions about file-system boundaries and GNU vs. non-GNU tools;

diff -r ffb4f2b9b1d3 -r f4d4d6d6702b 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"