# HG changeset patch
# User wenzelm
# Date 1358171572 -3600
# Node ID 1cadc8a8b37767f318d0dab5c6455391988751f6
# Parent  05054cf8ca77fea95ca39f31b76af4b933b68217
avoid odd copies of local configuration or backup files;

diff -r 05054cf8ca77 -r 1cadc8a8b377 Admin/lib/Tools/makedist_cygwin
--- a/Admin/lib/Tools/makedist_cygwin	Mon Jan 14 14:46:22 2013 +0100
+++ b/Admin/lib/Tools/makedist_cygwin	Mon Jan 14 14:52:52 2013 +0100
@@ -63,7 +63,7 @@
 
 # patches
 
-for NAME in hosts protocols services networks
+for NAME in hosts protocols services networks passwd group
 do
   rm "$TARGET/etc/$NAME"
 done
@@ -72,7 +72,10 @@
 
 rm "$TARGET/Cygwin.bat"
 
-cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/." "$TARGET/isabelle/."
+for NAME in init.bat postinstall rebaseall
+do
+  cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/$NAME" "$TARGET/isabelle/."
+done
 
 
 # archive