avoid odd copies of local configuration or backup files;
authorwenzelm
Mon, 14 Jan 2013 14:52:52 +0100
changeset 50887 1cadc8a8b377
parent 50886 05054cf8ca77
child 50888 bfe84bbd010b
avoid odd copies of local configuration or backup files;
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