Admin/lib/Tools/makedist_cygwin
Fri, 11 Jan 2013 22:38:12 +0100 wenzelm prefer MS-DOS-style temp;
Fri, 11 Jan 2013 22:23:03 +0100 wenzelm more Cygwin packages to help out in a pitch -- NB: make is still needed for legacy usedir;
Fri, 11 Jan 2013 14:54:52 +0100 wenzelm refer to cygwin mirror with static copy of setup.ini;
Thu, 10 Jan 2013 21:14:01 +0100 wenzelm tuned;
Thu, 10 Jan 2013 19:07:44 +0100 wenzelm clarified cygwin/isabelle scripts;
Thu, 10 Jan 2013 17:53:15 +0100 wenzelm more systematic makedist_cygwin;
less more (0) tip