Admin/lib/Tools/makedist_cygwin
changeset 50892 9a7d81d66d09
parent 50887 1cadc8a8b377
child 50958 af59600d8955
--- a/Admin/lib/Tools/makedist_cygwin	Mon Jan 14 20:12:18 2013 +0100
+++ b/Admin/lib/Tools/makedist_cygwin	Mon Jan 14 21:37:42 2013 +0100
@@ -72,11 +72,6 @@
 
 rm "$TARGET/Cygwin.bat"
 
-for NAME in init.bat postinstall rebaseall
-do
-  cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/$NAME" "$TARGET/isabelle/."
-done
-
 
 # archive