Admin/lib/Tools/makedist_cygwin
changeset 57027 80ffda443738
parent 53659 85ae414b0363
child 57048 7bd165c32e99
--- a/Admin/lib/Tools/makedist_cygwin	Tue May 20 20:05:43 2014 +0200
+++ b/Admin/lib/Tools/makedist_cygwin	Tue May 20 21:13:21 2014 +0200
@@ -4,7 +4,7 @@
 
 ## global parameters
 
-CYGWIN_MIRROR="http://isabelle.in.tum.de/cygwin_2013-1"
+CYGWIN_MIRROR="http://isabelle.in.tum.de/cygwin_2014"
 
 
 ## diagnostics
@@ -68,8 +68,6 @@
   rm "$TARGET/etc/$NAME"
 done
 
-ln -s cygperl5_14.dll "$TARGET/bin/cygperl5_14_2.dll"
-
 rm "$TARGET/Cygwin.bat"