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"