prefer MS-DOS-style temp;
authorwenzelm
Fri, 11 Jan 2013 22:38:12 +0100 (2013-01-11)
changeset 50839 9cc70b273e90
parent 50838 ad959a8b951e
child 50840 a5cc092156da
child 50842 777c6026ca93
prefer MS-DOS-style temp;
Admin/lib/Tools/makedist_cygwin
--- a/Admin/lib/Tools/makedist_cygwin	Fri Jan 11 22:23:03 2013 +0100
+++ b/Admin/lib/Tools/makedist_cygwin	Fri Jan 11 22:38:12 2013 +0100
@@ -53,7 +53,7 @@
 
 "$TARGET/isabelle/cygwin.exe" \
   --site "$CYGWIN_MIRROR" --no-verify \
-  --local-package-dir 'C:\tmp' \
+  --local-package-dir 'C:\temp' \
   --root "$(cygpath -w "$TARGET")" \
   --packages libgmp3,make,perl,python,rlwrap,vim \
   --no-shortcuts --no-startmenu --no-desktop --quiet-mode